cvc5.git
14 years agosimplification minisat
Dejan Jovanović [Sat, 13 Feb 2010 21:30:18 +0000 (21:30 +0000)]
simplification minisat

14 years agoImprovements to CNF conversion when already in CNF
Dejan Jovanović [Sat, 13 Feb 2010 00:55:40 +0000 (00:55 +0000)]
Improvements to CNF conversion when already in CNF

14 years agobuild fix
Dejan Jovanović [Fri, 12 Feb 2010 20:30:24 +0000 (20:30 +0000)]
build fix

14 years agoFix to compile out Debug(...) << ... statements in optimized mode. Someone please...
Dejan Jovanović [Fri, 12 Feb 2010 20:26:56 +0000 (20:26 +0000)]
Fix to compile out Debug(...) << ... statements in optimized mode. Someone please look to see if it makes sense.

14 years agoChanges to hashing that solve the xinetd boolean benchmark in 14s (from ~25min)....
Dejan Jovanović [Fri, 12 Feb 2010 01:07:22 +0000 (01:07 +0000)]
Changes to hashing that solve the xinetd boolean benchmark in 14s (from ~25min). Switched to standard hash_set, hash_map, new hash for the vector of node values (from boost), changed the hash for nodes to be over id's, all the hash values are now size_t. The parser is down from 11s to 10s on the benchmark, so most of the solve time is parsing and we need to figure this out.

14 years agosvn ignore
Dejan Jovanović [Thu, 11 Feb 2010 21:19:48 +0000 (21:19 +0000)]
svn ignore

14 years agoAdding precedence regressions
Christopher L. Conway [Thu, 11 Feb 2010 17:10:36 +0000 (17:10 +0000)]
Adding precedence regressions

14 years agonote on setup(); for discussion at 2010.02.11 meeting
Morgan Deters [Wed, 10 Feb 2010 22:22:14 +0000 (22:22 +0000)]
note on setup(); for discussion at 2010.02.11 meeting

14 years agosvn:ignore for build stuff; add Liana to AUTHORS
Morgan Deters [Wed, 10 Feb 2010 22:21:41 +0000 (22:21 +0000)]
svn:ignore for build stuff; add Liana to AUTHORS

14 years agofixing annoying eclipse build settings, no more broken pipe errors with these settings
Dejan Jovanović [Wed, 10 Feb 2010 03:52:27 +0000 (03:52 +0000)]
fixing annoying eclipse build settings, no more broken pipe errors with these settings

14 years agoAdded calls to destructor in CDList plus optional flag to disable.
Clark Barrett [Wed, 10 Feb 2010 00:33:01 +0000 (00:33 +0000)]
Added calls to destructor in CDList plus optional flag to disable.

14 years agoChanges to the CNF conversion and the SAT solver. All regression pass now, and we...
Dejan Jovanović [Tue, 9 Feb 2010 23:07:33 +0000 (23:07 +0000)]
Changes to the CNF conversion and the SAT solver. All regression pass now, and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser.

14 years agoremoving other pieces of autotools stuff to fix bug #24
Morgan Deters [Tue, 9 Feb 2010 22:02:34 +0000 (22:02 +0000)]
removing other pieces of autotools stuff to fix bug #24

14 years agomoving built-in kinds out of the kind.h prologue/middle for uniformity; added TUPLE...
Morgan Deters [Tue, 9 Feb 2010 19:20:32 +0000 (19:20 +0000)]
moving built-in kinds out of the kind.h prologue/middle for uniformity; added TUPLE built-in

14 years agoempty stubs for push and pop to fix the build fail
Dejan Jovanović [Tue, 9 Feb 2010 03:27:16 +0000 (03:27 +0000)]
empty stubs for push and pop to fix the build fail

14 years agoDisabling the failing test case for the context.
Dejan Jovanović [Mon, 8 Feb 2010 18:47:48 +0000 (18:47 +0000)]
Disabling the failing test case for the context.

14 years agoFixing the test case, it had a unary or. The cnf converter should be adapted to handl...
Dejan Jovanović [Mon, 8 Feb 2010 18:47:21 +0000 (18:47 +0000)]
Fixing the test case, it had a unary or. The cnf converter should be adapted to handle cases like this.

14 years agoPush/Pop parsing and commands
Dejan Jovanović [Mon, 8 Feb 2010 18:46:32 +0000 (18:46 +0000)]
Push/Pop parsing and commands

14 years agoMoving the template stuff back into the header in order to use CDList.
Dejan Jovanović [Mon, 8 Feb 2010 18:45:02 +0000 (18:45 +0000)]
Moving the template stuff back into the header in order to use CDList.

14 years agoDocumenting type.h/cpp
Christopher L. Conway [Sun, 7 Feb 2010 17:19:46 +0000 (17:19 +0000)]
Documenting type.h/cpp
Making Boolean and Kind types singletons

14 years agoforce sorting of AC_CONFIG_FILES, otherwise different computers generate the configur...
Morgan Deters [Sat, 6 Feb 2010 17:31:15 +0000 (17:31 +0000)]
force sorting of AC_CONFIG_FILES, otherwise different computers generate the configure script differently and we get useless commits of it; fix NodeBuilder memory leak in response to Kaustubh's expr code review (bug#15)

14 years agoPreliminary support for types in parser
Christopher L. Conway [Sat, 6 Feb 2010 03:06:07 +0000 (03:06 +0000)]
Preliminary support for types in parser

14 years agofinal fixes to addsourcedir source-directory-Makefile-generation script
Morgan Deters [Fri, 5 Feb 2010 23:21:55 +0000 (23:21 +0000)]
final fixes to addsourcedir source-directory-Makefile-generation script

14 years agoauto-generated list of AC_CONFIG_FILES so that you needn't add each recursive Makefil...
Morgan Deters [Fri, 5 Feb 2010 22:31:33 +0000 (22:31 +0000)]
auto-generated list of AC_CONFIG_FILES so that you needn't add each recursive Makefile to configure.ac

14 years agoautomatic generator script for sourcedir Makefiles and Makefile.ams
Morgan Deters [Fri, 5 Feb 2010 22:30:22 +0000 (22:30 +0000)]
automatic generator script for sourcedir Makefiles and Makefile.ams

14 years agoremove the last vestiges of support for "make build-profile" without first configurin...
Morgan Deters [Fri, 5 Feb 2010 21:16:56 +0000 (21:16 +0000)]
remove the last vestiges of support for "make build-profile" without first configuring the build-profile, simplifying the build process and closing bug 21

14 years agominor interface changes to TheoryEngine/Theory after meeting and conversation with Tim
Morgan Deters [Thu, 4 Feb 2010 23:59:41 +0000 (23:59 +0000)]
minor interface changes to TheoryEngine/Theory after meeting and conversation with Tim

14 years agofix run_regression script
Morgan Deters [Thu, 4 Feb 2010 23:50:25 +0000 (23:50 +0000)]
fix run_regression script

14 years agobeautification of the prop engine
Dejan Jovanović [Thu, 4 Feb 2010 23:50:23 +0000 (23:50 +0000)]
beautification of the prop engine

14 years agoassign expected-status to regressions
Morgan Deters [Thu, 4 Feb 2010 23:31:00 +0000 (23:31 +0000)]
assign expected-status to regressions

14 years agobuild system for multi-level regressions
Morgan Deters [Thu, 4 Feb 2010 23:29:47 +0000 (23:29 +0000)]
build system for multi-level regressions

14 years agoremove warnings from use of __gnu_cxx::hash_map<>; also spacing fixes in symbol table
Morgan Deters [Thu, 4 Feb 2010 22:14:28 +0000 (22:14 +0000)]
remove warnings from use of __gnu_cxx::hash_map<>; also spacing fixes in symbol table

14 years agoremove -*- c++ -*- emacs tag from source files (it overrides cvc4-c++-editing-mode...
Morgan Deters [Thu, 4 Feb 2010 22:10:47 +0000 (22:10 +0000)]
remove -*- c++ -*- emacs tag from source files (it overrides cvc4-c++-editing-mode from contrib/editing-with-emacs

14 years agoChanged mapping from atoms to literals in the prop engine to be atoms to vars.
Tim King [Thu, 4 Feb 2010 21:03:07 +0000 (21:03 +0000)]
Changed mapping from atoms to literals in the prop engine to be atoms to vars.

14 years agoMoved regressions into various levels based on running time.
Tim King [Thu, 4 Feb 2010 21:01:04 +0000 (21:01 +0000)]
Moved regressions into various levels based on running time.

14 years agotest infrastructure updated for multiple-level regressions
Morgan Deters [Thu, 4 Feb 2010 19:01:55 +0000 (19:01 +0000)]
test infrastructure updated for multiple-level regressions

14 years agominor cleanup; give the main driver a different exit code for SAT-INVALID/UNSAT-VALID
Morgan Deters [Thu, 4 Feb 2010 03:47:41 +0000 (03:47 +0000)]
minor cleanup; give the main driver a different exit code for SAT-INVALID/UNSAT-VALID

14 years agosrc/expr/kind.h is now automatically generated.
Morgan Deters [Thu, 4 Feb 2010 03:31:38 +0000 (03:31 +0000)]
src/expr/kind.h is now automatically generated.

Build src/expr before src/util.

Moved CVC4::Command to the expr package.

Re-quieted the "result is sat/invalid" etc. from PropEngine (this is
now done at the main driver level).

Added file-level documentation to Antlr sources

When built for debug, spin on SEGV instead of aborting.  Really useful
for debugging problems that crop up only on long runs.  Added
'--segv-nospin' to override this spinning so that "make check,"
nightly regressions, etc. don't hang when built with debug.

Updated src/main/about.h for 2010.

14 years agominor fix for update-copyright.pl; ran update-copyright.pl on all sources; regenerate...
Morgan Deters [Thu, 4 Feb 2010 02:58:12 +0000 (02:58 +0000)]
minor fix for update-copyright.pl; ran update-copyright.pl on all sources; regenerated configure script

14 years agoadded bool and arith theory makefiles to AC_CONFIG_FILES in configure.ac
Morgan Deters [Thu, 4 Feb 2010 02:47:30 +0000 (02:47 +0000)]
added bool and arith theory makefiles to AC_CONFIG_FILES in configure.ac

14 years agoAdded theory output channel interfaces and "Interrupted" exception.
Morgan Deters [Thu, 4 Feb 2010 02:46:17 +0000 (02:46 +0000)]
Added theory output channel interfaces and "Interrupted" exception.

Updated contrib/update-copyright to handle Antlr (.g) parser/lexer inputs.
Updated copyright year.

Added a new "bool" theory (right now just to hold a kind.h contribution).

Added "kinds" files to UF and the new "bool" theory.

14 years agoFixes to the cnf converter. Also a barebones utility for printing out a satisifying...
Tim King [Thu, 4 Feb 2010 00:47:45 +0000 (00:47 +0000)]
Fixes to the cnf converter. Also a barebones utility for printing out a satisifying model.

14 years agoAdding extra test to parser
Christopher L. Conway [Wed, 3 Feb 2010 23:52:16 +0000 (23:52 +0000)]
Adding extra test to parser

14 years agoadding an option to minisat to not do any debug checks/output
Dejan Jovanović [Wed, 3 Feb 2010 23:45:53 +0000 (23:45 +0000)]
adding an option to minisat to not do any debug checks/output

14 years agoFixing bad commit
Christopher L. Conway [Wed, 3 Feb 2010 23:43:43 +0000 (23:43 +0000)]
Fixing bad commit

14 years agoAdding functions/predicates to SMT grammar
Christopher L. Conway [Wed, 3 Feb 2010 22:46:36 +0000 (22:46 +0000)]
Adding functions/predicates to SMT grammar

14 years agoAddressed many of the concerns of bug 10 (build system code review).
Morgan Deters [Wed, 3 Feb 2010 22:20:25 +0000 (22:20 +0000)]
Addressed many of the concerns of bug 10 (build system code review).
Some parts split into other bugs: 19, 20, 21.

Addressed concerns of bug 11 (util package code review).

Slight parser source file modifications: file comments, #included
headers in generated parsers/lexers

Added CVC4::Result propagation back through
MiniSat->PropEngine->SmtEngine->main().  Silenced MiniSat when
verbosity is not requested.

14 years agoELSEIF support and parser debugging with '-d parser'
Dejan Jovanović [Wed, 3 Feb 2010 22:10:21 +0000 (22:10 +0000)]
ELSEIF support and parser debugging with '-d parser'

14 years agosimple ITE parsing
Dejan Jovanović [Wed, 3 Feb 2010 19:50:44 +0000 (19:50 +0000)]
simple ITE parsing

14 years agoBy popular demand, I also added a printAst to Expr.
Tim King [Wed, 3 Feb 2010 19:41:14 +0000 (19:41 +0000)]
By popular demand, I also added a printAst to Expr.

14 years agoI hacked in a temporary way to restart minisat for multiple queries.
Tim King [Wed, 3 Feb 2010 19:25:50 +0000 (19:25 +0000)]
I hacked in a temporary way to restart minisat for multiple queries.

14 years agoWithin node I added printAst(..) for general purpose debugging use throughout the...
Tim King [Wed, 3 Feb 2010 19:23:45 +0000 (19:23 +0000)]
Within node I added printAst(..) for general purpose debugging use throughout the code. I also added debugPrint() to Node for use within gdb.

14 years agoEnabled more regress tests. Takes 26s on my machine to run a make -k check in debug...
Tim King [Wed, 3 Feb 2010 19:19:36 +0000 (19:19 +0000)]
Enabled more regress tests. Takes 26s on my machine to run a make -k check in debug mode.  All regress tests currently pass.

14 years agocontext_mm testing
Dejan Jovanović [Wed, 3 Feb 2010 00:49:38 +0000 (00:49 +0000)]
context_mm testing

14 years agosome more tests for the context.
Dejan Jovanović [Wed, 3 Feb 2010 00:15:15 +0000 (00:15 +0000)]
some more tests for the context.

14 years ago(no commit message)
Dejan Jovanović [Tue, 2 Feb 2010 22:50:35 +0000 (22:50 +0000)]

14 years agoFixed bug in context code
Clark Barrett [Tue, 2 Feb 2010 22:40:55 +0000 (22:40 +0000)]
Fixed bug in context code

14 years agofor tim
Dejan Jovanović [Tue, 2 Feb 2010 22:36:57 +0000 (22:36 +0000)]
for tim

14 years agobeginings of test for CDO. one fail
Dejan Jovanović [Tue, 2 Feb 2010 22:01:59 +0000 (22:01 +0000)]
beginings of test for CDO. one fail

14 years agoRethrow rewrite in antlr_parser. Taking LT(0) to locate the error causes the build...
Dejan Jovanović [Tue, 2 Feb 2010 21:00:02 +0000 (21:00 +0000)]
Rethrow rewrite in antlr_parser. Taking LT(0) to locate the error causes the build to break on 64-bit machines. Changed to LT(1), it works now, but i'll ask around how this actually works.

14 years agoSwitched cnf conversion to go through CnfStream.
Tim King [Tue, 2 Feb 2010 20:56:47 +0000 (20:56 +0000)]
Switched cnf conversion to go through CnfStream.

14 years agoMinor changes to parser
Christopher L. Conway [Tue, 2 Feb 2010 20:04:18 +0000 (20:04 +0000)]
Minor changes to parser

14 years agoAdding support for escapes in string literals (strings like "\n\t\"")
Dejan Jovanović [Tue, 2 Feb 2010 19:12:09 +0000 (19:12 +0000)]
Adding support for escapes in string literals (strings like "\n\t\"")

14 years agoFixed compile errors
Clark Barrett [Tue, 2 Feb 2010 02:10:28 +0000 (02:10 +0000)]
Fixed compile errors

14 years agoUpdates to context:
Clark Barrett [Tue, 2 Feb 2010 02:04:39 +0000 (02:04 +0000)]
Updates to context:
  Use vector instead of linked list for Scopes
  Added CDO and CDList templates

14 years agoFixing the CVC grammar for parsing Boolean expressions. All the associativity stufff...
Dejan Jovanović [Mon, 1 Feb 2010 21:58:47 +0000 (21:58 +0000)]
Fixing the CVC grammar for parsing Boolean expressions. All the associativity stufff is now in the grammar. All the parser tests pass now.

14 years agofix node manager code (bugzilla #15, comment #2) in case where there's a hash collisi...
Morgan Deters [Mon, 1 Feb 2010 17:28:15 +0000 (17:28 +0000)]
fix node manager code (bugzilla #15, comment #2) in case where there's a hash collision for distinct objects

14 years agoAdded this test back to avoid make check problems.
Tim King [Mon, 1 Feb 2010 17:20:14 +0000 (17:20 +0000)]
Added this test back to avoid make check problems.

14 years agocnf conversion (variable-introducing), cleanups, fixes to minisat calling for multipl...
Morgan Deters [Sat, 30 Jan 2010 02:22:25 +0000 (02:22 +0000)]
cnf conversion (variable-introducing), cleanups, fixes to minisat calling for multiple-query cases

14 years agoChecking in small test fixes for node_black
Tim King [Sat, 30 Jan 2010 00:05:31 +0000 (00:05 +0000)]
Checking in small test fixes for node_black

14 years agofixing the last context build problem, it compiles now
Dejan Jovanović [Fri, 29 Jan 2010 22:25:22 +0000 (22:25 +0000)]
fixing the last context build problem, it compiles now

14 years agoone more bug
Clark Barrett [Fri, 29 Jan 2010 22:04:43 +0000 (22:04 +0000)]
one more bug

14 years agoFixed compile errors
Clark Barrett [Fri, 29 Jan 2010 21:02:15 +0000 (21:02 +0000)]
Fixed compile errors

14 years agoAdding Makefile.in to svn:ignore
Christopher L. Conway [Fri, 29 Jan 2010 20:16:10 +0000 (20:16 +0000)]
Adding Makefile.in to svn:ignore

14 years agoAdding Makefile.in to svn:ignore
Christopher L. Conway [Fri, 29 Jan 2010 20:14:37 +0000 (20:14 +0000)]
Adding Makefile.in to svn:ignore

14 years agoFixing boolean operator precedences
Christopher L. Conway [Fri, 29 Jan 2010 20:05:46 +0000 (20:05 +0000)]
Fixing boolean operator precedences

14 years agoUpdate of context module
Clark Barrett [Fri, 29 Jan 2010 19:46:26 +0000 (19:46 +0000)]
Update of context module

14 years agofixed CNF conversion, and more modular; CNF conversion command line option; various...
Morgan Deters [Fri, 29 Jan 2010 00:05:16 +0000 (00:05 +0000)]
fixed CNF conversion, and more modular; CNF conversion command line option; various cleanups; renamed numChildren() to getNumChildren() and added it to NodeBuilder interface; fancier, non-exponential CNF conversion with variable introduction is still buggy (?)

14 years agoRemoving Makefile.in's
Christopher L. Conway [Thu, 28 Jan 2010 18:31:46 +0000 (18:31 +0000)]
Removing Makefile.in's

14 years agoReplacing hand-coded autogen.sh with buildconf version
Christopher L. Conway [Thu, 28 Jan 2010 17:38:25 +0000 (17:38 +0000)]
Replacing hand-coded autogen.sh with buildconf version

14 years agosupport "make check" in src/ subdirs for unit-testing of just that module; also suppo...
Morgan Deters [Wed, 27 Jan 2010 22:48:03 +0000 (22:48 +0000)]
support "make check" in src/ subdirs for unit-testing of just that module; also support synonyms for "make check" globally

14 years agotest framework fixes; bug 13 closed
Morgan Deters [Wed, 27 Jan 2010 22:12:33 +0000 (22:12 +0000)]
test framework fixes; bug 13 closed

14 years agoAdded additional tests to node_black.h. CVC4 currently passes all but 1 test.
Tim King [Wed, 27 Jan 2010 20:53:28 +0000 (20:53 +0000)]
Added additional tests to node_black.h. CVC4 currently passes all but 1 test.

14 years agoUndoing stupid commit mistake. Rolling back to -r 102 for test/unit/expr/node_black.h
Tim King [Tue, 26 Jan 2010 18:03:11 +0000 (18:03 +0000)]
Undoing stupid commit mistake.  Rolling back to -r 102 for test/unit/expr/node_black.h

14 years agoAdded test/regress/boolean.cvc
Tim King [Tue, 26 Jan 2010 17:55:28 +0000 (17:55 +0000)]
Added test/regress/boolean.cvc

14 years agocnf conversion
Morgan Deters [Tue, 26 Jan 2010 15:06:24 +0000 (15:06 +0000)]
cnf conversion

14 years agofixes to build structure, util classes, lots of fixes to Node and NodeBuilder. outst...
Morgan Deters [Tue, 26 Jan 2010 07:29:41 +0000 (07:29 +0000)]
fixes to build structure, util classes, lots of fixes to Node and NodeBuilder.  outstanding SEGVs fixed

14 years agominor fixes to scoped-context node manager
Morgan Deters [Mon, 25 Jan 2010 21:15:29 +0000 (21:15 +0000)]
minor fixes to scoped-context node manager

14 years agoscoped node managers
Morgan Deters [Mon, 25 Jan 2010 21:10:01 +0000 (21:10 +0000)]
scoped node managers

14 years agoAdded pure PL regression tests. Mostly CNF
Tim King [Sat, 23 Jan 2010 02:20:57 +0000 (02:20 +0000)]
Added pure PL regression tests. Mostly CNF

14 years agoAdded regression test
Tim King [Fri, 22 Jan 2010 22:43:37 +0000 (22:43 +0000)]
Added regression test

14 years agominor changes to Theory
Morgan Deters [Tue, 19 Jan 2010 15:10:49 +0000 (15:10 +0000)]
minor changes to Theory

14 years agoChanges to configure.ac from code review
Christopher L. Conway [Tue, 5 Jan 2010 02:37:35 +0000 (02:37 +0000)]
Changes to configure.ac from code review

14 years agoMore fixes fot the parser tests.
Dejan Jovanović [Fri, 18 Dec 2009 23:34:05 +0000 (23:34 +0000)]
More fixes fot the parser tests.

14 years agoChanging some deatils on the parser. Now we know we are done if command is null,...
Dejan Jovanović [Fri, 18 Dec 2009 20:40:02 +0000 (20:40 +0000)]
Changing some deatils on the parser. Now we know we are done if command is null, or expression is null.

14 years agoMore fixes
Dejan Jovanović [Fri, 18 Dec 2009 19:57:34 +0000 (19:57 +0000)]
More fixes

14 years agonumerous fixes to nodes; more coming
Morgan Deters [Fri, 18 Dec 2009 19:47:42 +0000 (19:47 +0000)]
numerous fixes to nodes; more coming

14 years agoUpdated parser tests, which are all kinds of FAIL
Christopher L. Conway [Fri, 18 Dec 2009 18:23:18 +0000 (18:23 +0000)]
Updated parser tests, which are all kinds of FAIL

14 years agoChanges to the parser tests to make them compile.
Dejan Jovanović [Fri, 18 Dec 2009 17:25:25 +0000 (17:25 +0000)]
Changes to the parser tests to make them compile.

14 years agomore build system fix-ups
Morgan Deters [Fri, 18 Dec 2009 14:10:10 +0000 (14:10 +0000)]
more build system fix-ups