anf2cnf:anf2cnf.git
6 years agoCOPYING file for distribution master
Luk Bettale [Tue, 27 Sep 2011 10:32:25 +0000 (12:32 +0200)]
COPYING file for distribution

6 years agoTODO file updated
Luk Bettale [Tue, 27 Sep 2011 10:32:05 +0000 (12:32 +0200)]
TODO file updated

6 years agoremoved measure and time-stamp
Luk Bettale [Tue, 27 Sep 2011 10:31:49 +0000 (12:31 +0200)]
removed measure and time-stamp

6 years agounsigned and const wherever possible. Added function xor_clean to produce CNF without...
Luk Bettale [Tue, 27 Sep 2011 10:31:03 +0000 (12:31 +0200)]
unsigned and const wherever possible. Added function xor_clean to produce CNF without xor clauses

6 years agognu99 to c99 (not compiler dependent) produces a warning for mkstemp
Luk Bettale [Tue, 27 Sep 2011 10:29:31 +0000 (12:29 +0200)]
gnu99 to c99 (not compiler dependent) produces a warning for mkstemp

6 years agoremoved time-stamp
Luk Bettale [Tue, 27 Sep 2011 10:29:10 +0000 (12:29 +0200)]
removed time-stamp

6 years agofeatures a shared library and installation
Luk Bettale [Tue, 27 Sep 2011 10:28:35 +0000 (12:28 +0200)]
features a shared library and installation

6 years agoremoved Time-stamp + unsigned int in loops
Luk Bettale [Tue, 27 Sep 2011 10:27:19 +0000 (12:27 +0200)]
removed Time-stamp + unsigned int in loops

6 years agoexample file
Luk Bettale [Tue, 27 Sep 2011 10:25:49 +0000 (12:25 +0200)]
example file

6 years agoREADME file added
Luk Bettale [Tue, 27 Sep 2011 10:24:17 +0000 (12:24 +0200)]
README file added

6 years agochanged name for ANF_var_is_unknown
Luk Bettale [Fri, 27 May 2011 06:53:03 +0000 (08:53 +0200)]
changed name for ANF_var_is_unknown

6 years agoanf2cnf function chosen in preprocess time, no useless function call, better types...
Luk Bettale [Fri, 27 May 2011 06:51:01 +0000 (08:51 +0200)]
anf2cnf function chosen in preprocess time, no useless function call, better types for Mate's helper function (bool, and const where relevant), unified syntax for Mate's function, renamed ANF_var_unknown to ANF_var_is_unknown

6 years agoerror in Makefile corrected (wrong target for bestbits)
Luk Bettale [Fri, 27 May 2011 06:49:12 +0000 (08:49 +0200)]
error in Makefile corrected (wrong target for bestbits)

6 years agoimprove libdatastruct (unsigned int for sizes, best hash size)
Luk Bettale [Fri, 27 May 2011 06:48:33 +0000 (08:48 +0200)]
improve libdatastruct (unsigned int for sizes, best hash size)

6 years agocleaning up programs for executable (useless spaces removed)
Luk Bettale [Fri, 27 May 2011 06:46:58 +0000 (08:46 +0200)]
cleaning up programs for executable (useless spaces removed)

6 years agoAdding MersenneTwister.h
Mate Soos [Fri, 1 Apr 2011 10:27:10 +0000 (12:27 +0200)]
Adding MersenneTwister.h

6 years agoBetter handling of UNSAT during score-determination
Mate Soos [Thu, 13 Jan 2011 19:43:03 +0000 (20:43 +0100)]
Better handling of UNSAT during score-determination

6 years agoBetter scores for best-bit
Mate Soos [Thu, 13 Jan 2011 19:42:50 +0000 (20:42 +0100)]
Better scores for best-bit

6 years agoBetter assert fail
Mate Soos [Thu, 13 Jan 2011 19:42:40 +0000 (20:42 +0100)]
Better assert fail

6 years agoOoops, a "return" was left in
Mate Soos [Sat, 8 Jan 2011 09:22:55 +0000 (10:22 +0100)]
Ooops, a "return" was left in

6 years agoPrint found best bits at every point
Mate Soos [Sat, 8 Jan 2011 09:15:13 +0000 (10:15 +0100)]
Print found best bits at every point

6 years agoAdding evaluation&propagation test code
Mate Soos [Sat, 8 Jan 2011 09:14:41 +0000 (10:14 +0100)]
Adding evaluation&propagation test code

I was not sure if propagate() recursively propagates or not

6 years agoFix:Random generation was not thread-safe
Mate Soos [Fri, 7 Jan 2011 11:16:11 +0000 (12:16 +0100)]
Fix:Random generation was not thread-safe

MTRand is only available as C++ in thread-safe version, so using that.

6 years agoGenerate at least 100 best bits
Mate Soos [Fri, 7 Jan 2011 00:05:45 +0000 (01:05 +0100)]
Generate at least 100 best bits

6 years agoUpping the ante -- best bits now seems to work
Mate Soos [Fri, 7 Jan 2011 00:03:22 +0000 (01:03 +0100)]
Upping the ante -- best bits now seems to work

6 years agoMore helper functions in libanf2cnf
Mate Soos [Fri, 7 Jan 2011 00:03:00 +0000 (01:03 +0100)]
More helper functions in libanf2cnf

6 years agoAdd bestbits.c to build list
Mate Soos [Thu, 6 Jan 2011 22:22:48 +0000 (23:22 +0100)]
Add bestbits.c to build list

6 years agoAdding preliminary best-bits calculator
Mate Soos [Thu, 6 Jan 2011 21:11:05 +0000 (22:11 +0100)]
Adding preliminary best-bits calculator

6 years agoAdding helper functions
Mate Soos [Thu, 6 Jan 2011 21:10:31 +0000 (22:10 +0100)]
Adding helper functions

6 years agoMerge branch 'master' of gitorious.org:anf2cnf/anf2cnf
Luk Bettale [Thu, 6 Jan 2011 17:52:27 +0000 (18:52 +0100)]
Merge branch 'master' of gitorious.org:anf2cnf/anf2cnf

6 years agouseless include and commented assert removed
Luk Bettale [Thu, 6 Jan 2011 17:51:48 +0000 (18:51 +0100)]
useless include and commented assert removed

6 years agoAdding CMakeLists.txt
Mate Soos [Thu, 6 Jan 2011 17:30:40 +0000 (18:30 +0100)]
Adding CMakeLists.txt

6 years agoMerge branch 'master' into HEAD
Mate Soos [Thu, 6 Jan 2011 17:29:19 +0000 (18:29 +0100)]
Merge branch 'master' into HEAD

6 years agoA //#define DEBUG should be in the top of file to allow easy DEBUG
Mate Soos [Thu, 6 Jan 2011 17:22:18 +0000 (18:22 +0100)]
A //#define DEBUG should be in the top of file to allow easy DEBUG

6 years agoRemove dangling spaces
Mate Soos [Thu, 6 Jan 2011 17:21:51 +0000 (18:21 +0100)]
Remove dangling spaces

6 years agoWhy have these functions static? Make them non-static
Mate Soos [Thu, 6 Jan 2011 17:20:47 +0000 (18:20 +0100)]
Why have these functions static? Make them non-static

6 years agoAdding anf2cnf binary based solver to anf2cnf.py
Mate Soos [Thu, 6 Jan 2011 17:20:04 +0000 (18:20 +0100)]
Adding anf2cnf binary based solver to anf2cnf.py

This is FAR faster than the python-based converter, and it also converts
in a much better way.

6 years agoUse
Luk Bettale [Thu, 6 Jan 2011 16:37:50 +0000 (17:37 +0100)]
Use
make -f debug.mk
to have the -g option
the Makefile is for "production"

6 years agotreating the new return value of ANF_parse + better error messages
Luk Bettale [Thu, 6 Jan 2011 16:36:45 +0000 (17:36 +0100)]
treating the new return value of ANF_parse + better error messages

6 years agoMerge branch 'master' of gitorious.org:anf2cnf/anf2cnf
Luk Bettale [Thu, 6 Jan 2011 16:36:14 +0000 (17:36 +0100)]
Merge branch 'master' of gitorious.org:anf2cnf/anf2cnf

Conflicts:
libanf2cnf.c

6 years agoreturn -1 in case of variables < 1
Luk Bettale [Thu, 6 Jan 2011 16:33:07 +0000 (17:33 +0100)]
return -1 in case of variables < 1

6 years agoMerge branch 'lukCorrect'
Mate Soos [Thu, 6 Jan 2011 09:52:55 +0000 (10:52 +0100)]
Merge branch 'lukCorrect'

6 years agoThe famous zero-sized mem allocation bug
Mate Soos [Thu, 6 Jan 2011 09:50:34 +0000 (10:50 +0100)]
The famous zero-sized mem allocation bug

Yay! if you allocate with calloc(0, sizeof(uint)), it may give you back
a NULL pointer, or a valid, strange pointer. Then, you can free NULL, so
using NULL as a way to mark that a pointer has already been freed (or
never allocated) is wrong, because in fact you can get NULL from a
"valid"(but really strange) calloc call. How we all love 0-sized
mallocs!

6 years agoBackporting to Luk version
Mate Soos [Thu, 6 Jan 2011 09:45:09 +0000 (10:45 +0100)]
Backporting to Luk version

6 years agoMerge branch 'seeminglyCorrect'
Mate Soos [Thu, 6 Jan 2011 09:35:40 +0000 (10:35 +0100)]
Merge branch 'seeminglyCorrect'

Conflicts:
libanf2cnf.c

6 years agobug correction (constant polynomials, etc)
Luk Bettale [Thu, 6 Jan 2011 08:14:03 +0000 (09:14 +0100)]
bug correction (constant polynomials, etc)

6 years agoremoved unused include
Luk Bettale [Thu, 6 Jan 2011 08:13:48 +0000 (09:13 +0100)]
removed unused include

6 years agoOoops, monomial_free was not a good idea to use here
Mate Soos [Thu, 6 Jan 2011 00:03:38 +0000 (01:03 +0100)]
Ooops, monomial_free was not a good idea to use here

6 years agoVariables start at 1 and above, not zero!
Mate Soos [Wed, 5 Jan 2011 23:53:51 +0000 (00:53 +0100)]
Variables start at 1 and above, not zero!

6 years agoprintf-s, commented out in case we need them
Mate Soos [Wed, 5 Jan 2011 23:52:07 +0000 (00:52 +0100)]
printf-s, commented out in case we need them

6 years agoMore setting of freed pointers to NULL
Mate Soos [Wed, 5 Jan 2011 23:51:41 +0000 (00:51 +0100)]
More setting of freed pointers to NULL

6 years agoMUCH more asserts, validations, etc
Mate Soos [Wed, 5 Jan 2011 23:50:00 +0000 (00:50 +0100)]
MUCH more asserts, validations, etc

6 years agoMore documentation
Mate Soos [Wed, 5 Jan 2011 23:48:58 +0000 (00:48 +0100)]
More documentation

6 years agoUse monomial_free
Mate Soos [Wed, 5 Jan 2011 23:48:38 +0000 (00:48 +0100)]
Use monomial_free

6 years agoLuk's program cannot eat var 0, only var 1 and above
Mate Soos [Wed, 5 Jan 2011 23:47:41 +0000 (00:47 +0100)]
Luk's program cannot eat var 0, only var 1 and above

6 years agoMore asserts -- Luk doesn't like asserts ;)
Mate Soos [Wed, 5 Jan 2011 22:02:39 +0000 (23:02 +0100)]
More asserts -- Luk doesn't like asserts ;)

6 years agoAdd delimiter-creator to SAGE script, to create files for executable
Mate Soos [Wed, 5 Jan 2011 22:00:46 +0000 (23:00 +0100)]
Add delimiter-creator to SAGE script, to create files for executable

The executable is MUCH faster and FAR more efficient than the anf2cnf
script. Use that to create the CNF, and to do all the crazy stuff on it

6 years agoAdd debug to executable
Mate Soos [Wed, 5 Jan 2011 22:00:32 +0000 (23:00 +0100)]
Add debug to executable

7 years agoassert after malloc, int to unsigned int in for loops
Luk Bettale [Wed, 3 Nov 2010 08:07:14 +0000 (09:07 +0100)]
assert after malloc, int to unsigned int in for loops

7 years agocryptominisat output even in non-debug mode
Luk Bettale [Wed, 3 Nov 2010 08:06:50 +0000 (09:06 +0100)]
cryptominisat output even in non-debug mode

7 years agoadded mkstemp checking + exit when cryptominisat is stopped
Luk Bettale [Thu, 28 Oct 2010 13:39:16 +0000 (15:39 +0200)]
added mkstemp checking + exit when cryptominisat is stopped

7 years agotime measurement using clock()
Luk Bettale [Thu, 28 Oct 2010 13:38:11 +0000 (15:38 +0200)]
time measurement using clock()

7 years agomaximum size of hashmap table put in libdatastruct
Luk Bettale [Thu, 28 Oct 2010 13:37:41 +0000 (15:37 +0200)]
maximum size of hashmap table put in libdatastruct

7 years agoSATsolve passes options to cryptominisat
Luk Bettale [Wed, 27 Oct 2010 16:04:57 +0000 (18:04 +0200)]
SATsolve passes options to cryptominisat

7 years agoadded propagate to only propagate at anf level and return a system with fresh variables
Luk Bettale [Tue, 26 Oct 2010 14:19:28 +0000 (16:19 +0200)]
added propagate to only propagate at anf level and return a system with fresh variables

7 years agoadded -O0 flag in debug.mk
Luk Bettale [Fri, 22 Oct 2010 13:51:40 +0000 (15:51 +0200)]
added -O0 flag in debug.mk

7 years agoprettier printing of time
Luk Bettale [Fri, 22 Oct 2010 13:51:26 +0000 (15:51 +0200)]
prettier printing of time

7 years agounified printing of solutions
Luk Bettale [Fri, 22 Oct 2010 13:51:08 +0000 (15:51 +0200)]
unified printing of solutions

7 years agomagma program to generate random systems
Luk Bettale [Fri, 22 Oct 2010 13:50:15 +0000 (15:50 +0200)]
magma program to generate random systems

7 years agoGBsolve target added
Luk Bettale [Fri, 22 Oct 2010 13:49:49 +0000 (15:49 +0200)]
GBsolve target added

7 years agosolver that uses Grobner Basis in Magma
Luk Bettale [Fri, 22 Oct 2010 13:49:14 +0000 (15:49 +0200)]
solver that uses Grobner Basis in Magma

7 years agoremoved debug information and added -O3
Luk Bettale [Thu, 21 Oct 2010 14:40:27 +0000 (16:40 +0200)]
removed debug information and added -O3

7 years agoadded debug.mk to separate debugging from "real" program
Luk Bettale [Thu, 21 Oct 2010 14:39:23 +0000 (16:39 +0200)]
added debug.mk to separate debugging from "real" program

7 years agofixed missing '|'
Luk Bettale [Thu, 21 Oct 2010 14:19:48 +0000 (16:19 +0200)]
fixed missing '|'

7 years agoutils.m adapted to both BooleanPolynomialRing and PolynomialRing
Luk Bettale [Thu, 21 Oct 2010 14:16:04 +0000 (16:16 +0200)]
utils.m adapted to both BooleanPolynomialRing and PolynomialRing

7 years agoremoved sync target
Luk Bettale [Thu, 21 Oct 2010 14:15:24 +0000 (16:15 +0200)]
removed sync target

7 years agoremoved done things in TODO list
Luk Bettale [Thu, 21 Oct 2010 08:47:08 +0000 (10:47 +0200)]
removed done things in TODO list

7 years agodump modified to accept variables with degree > 1 (algebraic closure)
Luk Bettale [Thu, 21 Oct 2010 08:44:58 +0000 (10:44 +0200)]
dump modified to accept variables with degree > 1 (algebraic closure)

7 years agoprinting functions renamed and separated
Luk Bettale [Thu, 21 Oct 2010 07:13:13 +0000 (09:13 +0200)]
printing functions renamed and separated
stop when inconclusive in looping

7 years agostops when cryptominisat becomes useless (with given options)
Luk Bettale [Wed, 20 Oct 2010 16:06:12 +0000 (18:06 +0200)]
stops when cryptominisat becomes useless (with given options)

7 years agosmall printing things
Luk Bettale [Wed, 20 Oct 2010 16:05:30 +0000 (18:05 +0200)]
small printing things

7 years agoprinting modification (DEBUG and CNF)
Luk Bettale [Wed, 20 Oct 2010 15:21:43 +0000 (17:21 +0200)]
printing modification (DEBUG and CNF)

7 years agoDEBUG flag, nicer name for tmp files, anf file also dumped
Luk Bettale [Wed, 20 Oct 2010 14:18:45 +0000 (16:18 +0200)]
DEBUG flag, nicer name for tmp files, anf file also dumped

7 years agofunctionnal program looping.c for iterating sat-solving after propagation of learnt...
Luk Bettale [Wed, 20 Oct 2010 13:41:12 +0000 (15:41 +0200)]
functionnal program looping.c for iterating sat-solving after propagation of learnt clauses

7 years agoadded :
Luk Bettale [Wed, 20 Oct 2010 13:39:54 +0000 (15:39 +0200)]
added :
parsing of learnt clauses
separate function for printing monomials
mapping literal / monomial in CNF printing

7 years agoadded -std=gnu99 in Makefile
Luk Bettale [Wed, 20 Oct 2010 13:38:32 +0000 (15:38 +0200)]
added -std=gnu99 in Makefile

7 years agoadded looping to do the reinjection, modified SATsolve and libanf2cnf to accept crypt...
Luk Bettale [Thu, 14 Oct 2010 16:55:54 +0000 (18:55 +0200)]
added looping to do the reinjection, modified SATsolve and libanf2cnf to accept cryptominisat output format

7 years agoTODO updated, (higher degree done)
Luk Bettale [Thu, 14 Oct 2010 13:35:43 +0000 (15:35 +0200)]
TODO updated, (higher degree done)
Makefile changed to clean befor sync
libanf2cnf modified to choose conversion function with at preprocessing

7 years agoreorganisation inside libanf2cnf.c + remove assert (to be reintroduced later)
Luk Bettale [Thu, 14 Oct 2010 13:20:29 +0000 (15:20 +0200)]
reorganisation inside libanf2cnf.c + remove assert (to be reintroduced later)

7 years agoMerge branch 'linkedlist'
Luk Bettale [Thu, 14 Oct 2010 12:46:23 +0000 (14:46 +0200)]
Merge branch 'linkedlist'

Conflicts:
SATsolve.c

7 years agoadded ifdef in headers + licence in libdatastruct.{h,c}
Luk Bettale [Thu, 14 Oct 2010 12:32:30 +0000 (14:32 +0200)]
added ifdef in headers + licence in libdatastruct.{h,c}

7 years agoremoved unimplemented function
Luk Bettale [Thu, 14 Oct 2010 11:53:26 +0000 (13:53 +0200)]
removed unimplemented function

7 years agoreformatting source code, removing chronoanf2cnf
Luk Bettale [Thu, 14 Oct 2010 11:49:59 +0000 (13:49 +0200)]
reformatting source code, removing chronoanf2cnf

7 years agoarray version, linked list version and hashmap version of anf2cnf.
Luk Bettale [Mon, 11 Oct 2010 09:29:46 +0000 (11:29 +0200)]
array version, linked list version and hashmap version of anf2cnf.
array version only for degree 2 polynomials
litteral -> literal
const modifier when relevant
renaming of several functions

7 years agolitteral -> literal
Luk Bettale [Wed, 29 Sep 2010 15:22:02 +0000 (17:22 +0200)]
litteral -> literal

7 years ago(dirty) linked list implementation of higher degree monomials in cnf (very slow)
Luk Bettale [Tue, 28 Sep 2010 10:11:12 +0000 (12:11 +0200)]
(dirty) linked list implementation of higher degree monomials in cnf (very slow)

7 years agoCorrecting monomial definitions' comments
Mate Soos [Mon, 27 Sep 2010 14:29:26 +0000 (16:29 +0200)]
Correcting monomial definitions' comments

It was displaying the same info for monomial definitions as for
polynomial definitions if the polynomial only consisted of a monomial

7 years agorenamed tabm to map
Luk Bettale [Fri, 24 Sep 2010 15:17:03 +0000 (17:17 +0200)]
renamed tabm to map

7 years agoavoid use of tabh
Luk Bettale [Fri, 24 Sep 2010 14:48:06 +0000 (16:48 +0200)]
avoid use of tabh

7 years agoextension for higher degree monomial when filling supp
Luk Bettale [Fri, 24 Sep 2010 12:42:02 +0000 (14:42 +0200)]
extension for higher degree monomial when filling supp