UNSAT found, expected SAT

[Broes De Cat]

tests/mxtests/SATmxtests/SATDijkstra.idp tests/mxtests/SATdijkstra2.idp tests/mxtests/SATmxtests/SATRobot.idp

[Broes De Cat]

Lots of fixes

fixes #55: partial functions and defined aggregates fixes #6: unnestterms did not do rewrite (previous commit)

Tests: moved tests around into more logical folder structure and names added parsertests separated long and short running tests. The long running tests are run only when building in release added scoping test added more tests on partial functions, arbitraties and equivalences (not all succeeding at the moment)

Added a CHECKTERMINATION macro to globaldata

Bugfixed tracing: added some documentation on how to get the trace moved the tracemonitor out of all of the commands and into the internalargument, to reduce dependencies. correct modelexpansion to use tracing on all relevant places (also calculate definitions) and work also for unsat

Bugfixed equivgrounder: was not working correctly if either of the subgrounders did not return exactly one literal. Now, the equivgrounder otherwise translates it into this case.

Bugfixed the groundtheory and policies: addFuncConstraints was fixed in the case that some interpretation is given or if a function is partial adding grounddefinition responsibility was moved out of the policies and into the ground theory and also works in the case that both separate rules and definition objects are passed to the theory.

Bugfixed printers: grounddefinition is visited correctly adding both a grounddefinition and more rules to it now works. ecnfprinting works better with supplied definition ids.

Moved propagation inference to a separate folder

Enhancement: syntax for defining functions was correct, there always has to be a functerm on the left hand side.

Updated pcsolver for bug in defined aggregates

Bugfixed derivesorts where changed flag was not set in some cases, leading to too few derivations.

→ 2f2f7003681d

[Broes De Cat]

Lots of fixes

fixes #55: partial functions and defined aggregates fixes #6: unnestterms did not do rewrite (previous commit)

Tests: moved tests around into more logical folder structure and names added parsertests separated long and short running tests. The long running tests are run only when building in release added scoping test added more tests on partial functions, arbitraties and equivalences (not all succeeding at the moment)

Added a CHECKTERMINATION macro to globaldata

Bugfixed tracing: added some documentation on how to get the trace moved the tracemonitor out of all of the commands and into the internalargument, to reduce dependencies. correct modelexpansion to use tracing on all relevant places (also calculate definitions) and work also for unsat

Bugfixed equivgrounder: was not working correctly if either of the subgrounders did not return exactly one literal. Now, the equivgrounder otherwise translates it into this case.

Bugfixed the groundtheory and policies: addFuncConstraints was fixed in the case that some interpretation is given or if a function is partial adding grounddefinition responsibility was moved out of the policies and into the ground theory and also works in the case that both separate rules and definition objects are passed to the theory.

Bugfixed printers: grounddefinition is visited correctly adding both a grounddefinition and more rules to it now works. ecnfprinting works better with supplied definition ids.

Moved propagation inference to a separate folder

Enhancement: syntax for defining functions was correct, there always has to be a functerm on the left hand side.

Updated pcsolver for bug in defined aggregates

Bugfixed derivesorts where changed flag was not set in some cases, leading to too few derivations.

→ 2f2f7003681d

[Broes De Cat]

Removing milestone: First Release 25/12/2011 (automated comment)