summaryrefslogtreecommitdiff
path: root/src/main
AgeCommit message (Collapse)Author
2011-09-29Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵Morgan Deters
and model gen also. I also expect this commit to fix bug #273. No performance change is expected on regressions with this commit, see http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
2011-09-21considerable bindings interface work, some improvements to buildMorgan Deters
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2011-09-02* Changing pre-registration to be context dependent -- it is called from the ↵Dejan Jovanović
SAT solver on every backtrack * Updated UF to handle the context dependent pre-registration * Additionally some small changes in order to satisfy warnings of the eclipse code analysis tool
2011-06-30some things I had laying around in a directory but never got committed; ↵Morgan Deters
minor fix-ups to documentation and some node stuff
2011-05-28include subversion information used for each build in the --show-config ↵Morgan Deters
output and as a banner in --interactive mode; intended to resolve confusion in cases where you don't know where a CVC4 binary came from
2011-05-13* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolioMorgan Deters
branch) * add Theory::isSharedTermFact() -- it currently always returns false, pending theory combination work * Add "unknown" cardinalities to Cardinality class * Fix run_regression script to handle CRLF line terminators on Macs (where sed is non-GNU) * Convert CRLF line terminators in datatypes regressions to LF
2011-05-05Merge from nonclausal-simplification-v2 branch:Morgan Deters
* Preprocessing-time, non-clausal, Boolean simplification round to support "quasi-non-linear rewrites" as discussed at last few meetings. * --simplification=none is the default for now, but we'll probably change that to --simplification=incremental. --simplification=batch is also a possibility. See --simplification=help for details. * RecursionBreaker<T> now uses a hash set for the seen trail. * Fixes to TLS stuff to support that. * Fixes to theory and SmtEngine documentation. * Fixes to stream indentation. * Other miscellaneous stuff.
2011-05-02Minor fixes to various parts of CVC4, including the removal of the uintptr_t ↵Morgan Deters
constructors for Type and Expr (which existed due to ANTLR limitations). These issues are now handled (as a hack, due to said limitations) in the parser rather than the CVC4 core.
2011-05-01minor fixes, plus experimental readline support in InteractiveShellMorgan Deters
2011-04-15parser/driver fixes for last commitMorgan Deters
2011-04-10merge from replay branchMorgan Deters
2011-04-04Add documentation to Node and TNode (closes bug #201).Morgan Deters
Also, only build doxygen documentation on stuff in src/, not test/ or contrib/ or anywhere else. Hopefully this turns our 3000+ page user manual into something a little more useful!
2011-04-01This commit is a merge from the "betterstats" branch, which:Morgan Deters
* Makes Options an "omnipresent thread-local global" (like the notion of the "current NodeManager" was already). Options::current() accesses this structure. * Removes Options from constructors and data structures everywhere (this cleans up a lot of things). * No longer uses StatisticsRegistry statically. An instance of the registry is created and linked to a NodeManager. * StatisticsRegistry::current() is similar to Options::current(), but the pointer is stowed in the NodeManager (rather than stored) * The static functions of StatisticsRegistry have been left, for backward compatibility; they now use the "current" statistics registry. * SmtEngine::getStatisticsRegistry() is a public accessor for the registry; this is needed by main() to reach in and get the registry, for flushing statistics at the end.
2011-03-30Add Valuation::getSatValue() so that theories can access the currentMorgan Deters
(propositional) assignment for theory atoms. Fixed Debug/Trace as discussed in bug ticket #252 and on the mailing list. This implementation leads to some compiler warnings in production builds, but these will be corrected in coming days. There appears to be a small speedup in the parser as a result of this fix: http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1902&reference_id=1886&p=5 Cleaned up a few CD Boolean attribute things. Various small fixes to coding guidelines / test coverage. This commit: * Resolves bug 252 (tracing not disabled in production builds) * Resolves bug 254 (implement CDAttrHash<>::BitIterator::find())
2011-03-03fix for bug #244, "Segfault if file cannot be found and --stats is on"Morgan Deters
2010-11-05Moving Options fiddling to options.hChristopher L. Conway
2010-11-04competition mode implies --no-checkingMorgan Deters
2010-10-31small fix to debug segfaultsMorgan Deters
2010-10-31maximize stack limit, handle SEGV signals on an alternate signal stack, and ↵Morgan Deters
try to diagnose stack overflow
2010-10-29minor fixes as a result of review of Chris's getType() rewrite; also fix ↵Morgan Deters
some macros to make various GCC versions happy
2010-10-28Changing NodeBuilder::debugCheckType() to maybeCheckType()Christopher L. Conway
Changing NodeManager/ExprManager constructors to take Options
2010-10-26Cleaning up some header filesChristopher L. Conway
2010-10-25for static linking of driver binary, list libmain.a first (fixes link errors ↵Morgan Deters
in last night's regressions)
2010-10-24Adding unit test for InteractiveShellChristopher L. Conway
2010-10-23Adding Parser::setInput and using it in InteractiveShell (Fixes: #225)Christopher L. Conway
Removing ParserBuilder::withStateFrom
2010-10-22Saving state between lines in interactive mode (Fixes: #223)Christopher L. Conway
2010-10-22Using Options in ParserBuilder and InteractiveShellChristopher L. Conway
2010-10-22Merging main/getopt.cpp, main/usage.h, and smt/options.h inChristopher L. Conway
util/options.h,cpp
2010-10-21* Option --no-type-checking now disables type checks in SmtEngineChristopher L. Conway
* Adding options --lazy-type-checking and --eager-type-checking to control type checking in NodeBuilder, which can now be enabled in production mode and disabled in debug mode * Option --no-checking implies --no-type-checking * Adding constructor SmtEngine(ExprManager* em) that uses default options
2010-10-20Changing --no-early-type-checking to --no-type-checkingChristopher L. Conway
Disabling type checking when --no-checking is given (Fixes: #221)
2010-10-20Adding detection of TTY vs. piped input for interactive modeChristopher L. Conway
2010-10-20Adding support for interactive modeChristopher L. Conway
2010-10-12with --stats, statistics are dumped for memouts and (normal) exceptions.Morgan Deters
2010-10-10additional model gen and SMT-LIBv2 compliance work: (get-assignment) now ↵Morgan Deters
supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command
2010-10-08* (define-fun...) now has proper type checking in non-debug buildsMorgan Deters
(resolves bug #212) * also closed some other type checking loopholes in SmtEngine * small fixes to define-sort (resolves bug #214) * infrastructural support for printing expressions in languages other than the internal representation language using an IO manipulator, e.g.: cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr; main() sets the output language for all streams to correspond to the input language * support delaying type checking in debug builds, so that one can debug the type checker itself (before it was difficult, because debug builds did all the type checking on Node creation!): new command-line flag --no-early-type-checking (only makes sense for debug builds) * disallowed copy-construction of ExprManager and NodeManager, and made other constructors explicit; previously it was easy to unintentionally create duplicate managers, with really weird results (i.e., disappearing attributes!)
2010-10-07type checking for define-fun in production builds; related to (and might ↵Morgan Deters
resolve) bug 212
2010-10-07SMT-LIBv2 (define-fun...) command now functional; does eager expansion at ↵Morgan Deters
preprocessing time
2010-10-05parser and core support for SMT-LIBv2 commands get-info, set-option, ↵Morgan Deters
get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
2010-10-03file header documentation regenerated with contributors names; no code ↵Morgan Deters
modified in this commit
2010-10-02dump statistics on abnormal output: unexpected exceptions, SEGV, ILL, memout...Morgan Deters
2010-10-01replacement implementation for clock_gettime() on mac os x, build ↵Morgan Deters
portability (resolving mac os x issues), code cleanup, fix compiler warnings
2010-09-27add workaround for systems (i.e., Mac OS X) that don't support __thread; ↵ACSYS
also configure script auto-detection of __thread support and syntax
2010-09-21remove assertion in TNode destructor and ensure all TNode methods check rc > ↵Morgan Deters
0 (resolves bug #200); on NodeManager/ExprManager side, no more prepareToBeDestroyed() / inDestruction
2010-09-21fix statistics-registry-related memory leaksMorgan Deters
2010-09-13statistics are now printed on timeout (SIGXCPU) and SIGINT if --stats is givenMorgan Deters
2010-08-19UF theory bug fixes, code cleanup, and extra debugging output.Morgan Deters
Enabled new UF theory by default. Added some UF regressions. Some work on the whole equality-over-bool-removed-in-favor-of-IFF thing. (Congruence closure module and other things have to handle IFF as a special case of equality, etc..) Added pre-rewriting to TheoryBool which rewrites: * (IFF true x) => x * (IFF false x) => (NOT x) * (IFF x true) => x * (IFF x false) => (NOT x) * (IFF x x) => true * (IFF x (NOT x)) => false * (IFF (NOT x) x) => false * (ITE true x y) => x * (ITE false x y) => y * (ITE cond x x) => x Added post-rewriting that does all of the above, plus normalize IFF and ITE: * (IFF x y) => (IFF y x), if y < x * (ITE (NOT cond) x y) => (ITE cond y x) (Note: ITEs survive the removal-of-ITEs pass only if they are Boolean-valued.) A little more debugging output from CNF stream, context pushes/pops, ITE removal. Some more documentation. Fixed some typos.
2010-08-17Merge from "cc" branch:Morgan Deters
CongruenceClosure implementation; CongruenceClosure white-box test. New UF theory implementation based on new CC module. This one supports predicates. The two UF implementations exist in parallel (they can be selected at runtime via the new command line option "--uf"). Added type infrastructure for TUPLE. Fixes to unit tests that failed in 16-August-2010 regressions. Needed to instantiate TheoryEngine with an Options structure, and explicitly call ->shutdown() on it before destruction (like the SMTEngine does). Fixed test makefiles to (1) perform all tests even in the presence of failures, (2) give proper summaries of subdirectory tests (e.g. regress0/uf and regress0/precedence) Other minor changes.
2010-07-06Fixed exit status for competition mode.Tim King
2010-07-06add Configuration::isCompetitionBuild() and some main driver fixesMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback