summaryrefslogtreecommitdiff
path: root/test/regress/regress1
AgeCommit message (Collapse)Author
2017-12-07Fixes related to SyGuS + real arithmetic (#1432)Andrew Reynolds
2017-11-13Argument Relevance for Synthesis Conjectures (#1311)Andrew Reynolds
* Initial work on conjecture-specific symmetry breaking. * More infrastructure, working on process term. * Flattening. * Process defs * More setup * Fixes. * Sketching * Generalize to inference of argument definitions. * More, separate conjunct processing per synth function. * Single occurrence variables. * Assign relevance. * Document, connecting. * Connecting to grammar construction. * Enabled, add regressions. * Fix regressions. * Clang format. * Add regress1, minor. * Fix * Two passes. * Fix * Note * Improve check match, make single var occurrence more conservative. * Add regression. * Clang format * Minor comments * Update regression to new option. * Undo grammar cons changes. * Enable irrelevant args. * Improvements. * Format * Minor
2017-11-03Sygus clean main (#1297)Andrew Reynolds
* Remove front end hack for sygus. * Remove other hack, add sygus solution output mode. * Clang format * Minor * Fix * Minor * Remove unused field.
2017-10-20Make Sygus conjectures higher-order (#1244)Andrew Reynolds
* Represent sygus synthesis conjectures using higher-order quantification, remove associated hacks. * Minor fix * Fix bug in Node::hasBoundVar for non-ground operators. * Add regression. * Address review. * Apply clang format.
2017-10-12Sygus logics (#1226)Andrew Reynolds
* Allow any smt2 logic to be a sygus logic. Add non-linear SyGuS regressions. * Minor * Add case for reals, comment. * Fix regress1.
2017-08-04Set default language to smt lib 2.6 (including as a base language for ↵ajreynol
sygus), update regressions.
2017-07-10Merge ntExt branch. Adds support for transcendental functions. Refactoring ↵ajreynol
of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ↵ajreynol
decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
2017-05-31Minor change to defaults, update smt comp script, minor changes to options ↵ajreynol
in regressions.
2017-05-15Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802.ajreynol
2017-03-24Add some regressions. Minor.ajreynol
2017-03-15Fix regress1 Makefile for rewriterules, fixes bug 783.ajreynol
2017-01-04Marking regression test files as non-executable.Tim King
2016-12-12Fix split-find-unsat-w-emp testAndres Notzli
Commit 2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa did not update the split-find-unsat-w-emp test, this commit fixes that.
2016-10-21Fix/add missing makefiles.ajreynol
2016-10-21Move slow regress0 benchmarks to regress1, increment regress1 through regress3.ajreynol
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof ↵Morgan Deters
generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line
2013-12-09mv prp to regress1Kshitij Bansal
2013-11-11Change exit status to be more consistent with other command-line tools: 0 ↵Morgan Deters
success, nonzero error
2013-09-18Support a personal build configuration and make rules.Morgan Deters
2013-09-13Move some regress benchmarks around that took too long, other test cleanup.Morgan Deters
2013-02-16Some cleanup and copyright updatingMorgan Deters
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-01-28some fixes for win32, including ability to "make check" win32 builds via wineMorgan Deters
2012-08-28fix regression tests for automake 1.11 and automake 1.12---both versions ↵Morgan Deters
should work now
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure. Adds theory instantiators to many theories. Adds the UF strong solver.
2012-04-05Support to test the "dumper" mechanism in regressions (feeding dump output ↵Morgan Deters
back in) by doing "make regress RUN_REGRESSION_ARGS=--dump"
2012-02-20portfolio mergeMorgan Deters
2012-02-15This commit merges into trunk the branch branches/arithmetic/integers2 from ↵Tim King
r2650 to r2779. - This excludes revision 2777. This revision had some strange performance implications and was delaying the merge. - This includes the new DioSolver. The DioSolver can discover conflicts, produce substitutions, and produce cuts. - The DioSolver can be disabled at command line using --disable-dio-solver. - This includes a number of changes to the arithmetic normal form. - The Integer class features a number of new number theoretic function. - This commit includes a few rather loud warning. I will do my best to take care of them today.
2012-01-25Adding regress1 test ooo.rf6.smt2.Tim King
2011-12-15Partial fix in arithmetic for propagating shared terms. This partially ↵Tim King
resolves bug 289. Adds failing tests to regress1.
2011-11-30Added a failing regression test corresponding to bug 289.Tim King
2011-10-29support for proof regressions in other parts of the test treeMorgan Deters
2011-03-26fix typoMorgan Deters
2011-03-25This is a merge from the "theoryfixes+cdattrhash" branch. The changesMorgan Deters
are somewhat disparate but belonged on the same branch because they were held back from trunk all for the same reason (to keep the trunk stable for furious bitvector development). Dejan has now given me the go-ahead for a merge. ========================================= THIS COMMIT CHANGES THE THEORY INTERFACE! ========================================= Theory constructors are expected to take an additional "Valuation*" parameter that each Theory should send along to the base class constructor. The base class Theory keeps the Valuation* in a d_valuation field for use by it and by its derived classes. Theory::getValue() no longer takes a Valuation* (it is expected to use d_valuation instead). This allows other theory functions to take advantage of getValue() for debugging or heuristic purposes. TODO BEFORE MERGE TO TRUNK: ****implement BitIterator find() in CDAttrHash<bool>. Specifically: * Added QF_BV support for SMT-LIB v2. * Two adjustments to the theory interface as requested by Tim King: 1. As described above. 2. Theories now have const access to the fact queue through base class functions facts_begin() and facts_end(); useful for debugging. * Added an "Asserted" attribute so that theories can check if something has been asserted or not (and therefore not propagate it). However, this has been disabled for now, pending more data on the overhead of it, and pending discussion at the 3/25/2011 meeting. * Do not define NDEBUG in MiniSat in assertion-enabled builds (so that MiniSat asserts are evaluated). * As a result of the new MiniSat assertions, some --incremental regressions had to be disabled; also, some bitvectors ?!! * Bug 71 is resolved by adding a specialization for CDAttrHash<> in the attribute package. * Fixes for some warnings flagged by clang. * System tests have arrived! So far mainly infrastructure for having system tests, but there is a system test aimed at improving code coverage of the printer package. * Minor other adjustments to documentation and coding to be more conformant to CVC4 policy. Tests have been performed to demonstrate that these changes have no or negligible effect on performance. In particular, changing the CDAttrHash<> doesn't have any real effect on performance or memory right now, since there is only one context-dependent boolean flag (as soon as another is added, the effect is noticeable but probably still slight).
2010-10-13Added test/regress/regress1/arith and populated it with some fast SMT LIB ↵Tim King
problems.
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-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-06add regressions from bug reportsMorgan Deters
2010-07-04assigning benchmark statusesMorgan Deters
2010-07-04make dist && make distcheck functional, other fixesMorgan Deters
2010-06-17fix some minor annoyances in the regression test Makefiles; add some ↵Morgan Deters
documentation
2010-05-29Adding a couple of example from fuzzsmt to regress1.Tim King
2010-04-04* Node::isAtomic() now looks at an "atomic" attribute of argumentsMorgan Deters
instead of assuming it's atomic based on kind. Atomicity is determined at node building time. Fixes bug #81. If this is determined to make node building too slow, we can allocate another attribute "AtomicHasBeenComputed" to lazily compute atomicity. * TheoryImpl<> has gone away. Theory implementations now derive from Theory directly and share a single RegisteredAttr attribute for term registration (which shouldn't overlap: every term is "owned" by exactly one Theory). Fixes bug #79. * Additional atomicity tests in ExprBlack unit test. * More appropriate whitebox testing for attribute ID assignment (AttributeWhite unit test). * Better (and more correct) assertion checking in NodeBuilderBlack. * run-regression script now checks exit status against what's provided in "% EXIT: " gesture in .cvc input files, and stderr against "% EXPECT-ERROR: ". These can be used to support intended failures. Fixes bug #84. Also add "% EXIT: " gestures to all .cvc regressions in repository. * Solved some "control reaches end of non-void function" warnings in src/parser/bounded_token_buffer.cpp by replacing "AlwaysAssert(false)" with "Unreachable()" (which is known statically to never return normally). * Regression tests now use the cvc4 binary under builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which may not be properly installed yet at that point of the build. (Partially fixes bug #46.) * -fvisibility=hidden is now included by configure.ac instead of each Makefile.am, which will make it easier to support platforms (e.g. cygwin) that do things a different way. * TheoryUF code formatting. (re: my code review bug #64) * CDMap<> is leaking memory again, pending a fix for bug #85 in the context subsystem. (To avoid serious errors, can't free context objects.) * add ContextWhite unit test for bug #85 (though it's currently "defanged," awaiting the bugfix) * Minor documentation, other cleanup.
2010-03-30Removing unnecessary .gitignoresChristopher L. Conway
2010-03-30Merging from branches/antlr3 (r246:354)Christopher L. Conway
2010-02-04assign expected-status to regressionsMorgan Deters
2010-02-04build system for multi-level regressionsMorgan Deters
2010-02-04Moved regressions into various levels based on running time.Tim King
2010-02-04test infrastructure updated for multiple-level regressionsMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback