Age | Commit message (Expand) | Author |
2016-06-17 | Cleanup from last commit, treat sep.nil as variable kind. | ajreynol |
2016-06-17 | Support for separation logic. Enable cbqi by default for pure BV. | ajreynol |
2016-05-15 | Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. En... | ajreynol |
2016-05-06 | Minor clean up, fixes related to sygus. | ajreynol |
2016-05-05 | Compute term indices lazily in TermDb. Optimization for qcf to recognize irre... | ajreynol |
2016-05-05 | Removing a null pointer reference that was found by -fsanitize=null. | Tim King |
2016-04-13 | Update native language support for strings. | ajreynol |
2016-04-09 | cardinality operation for finite sets (based on my thesis / ijcar16 paper) | Kshitij Bansal |
2016-04-03 | Updating the copyright headers and scripts. | Tim King |
2016-03-08 | Extend synthesis solver to handle single invocation with additional universal... | ajreynol |
2016-02-16 | Public interface for quantifier elimination. Minor changes to datatypes rewr... | ajreynol |
2016-02-15 | Minor change to last commit | ajreynol |
2016-02-15 | Eliminate most of the internal representation infrastructure for tuples and r... | ajreynol |
2016-02-02 | Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ... | Tim King |
2016-02-01 | Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a simpler build p... | Tim King |
2016-01-28 | Adding listeners to Options. | Tim King |
2016-01-08 | Adding a new Listener utility class. Changing the ResourceManager to use List... | Tim King |
2016-01-08 | Disabling the RESTART command. | Tim King |
2016-01-06 | Improving the documentation of the CVC command CONTINUE. | Tim King |
2015-12-30 | Shuffling around public vs. private headers | Tim King |
2015-12-18 | Modifying emptyset.h and sexpr. Adding SetLanguage. | Tim King |
2015-12-15 | Breaking the include cycle between Record and Expr. | Tim King |
2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
2015-12-03 | Removing the generated directory from the parsers. | Tim King |
2015-11-26 | Front-end support for get-value of sort cardinality, minor fixes for sygus so... | ajreynol |
2015-11-23 | Isolating the dependencies on CVC4_ANTLR3_OLD_INPUT_STREAM. Also freeing more... | Tim King |
2015-09-24 | Counterexample-guided instantiation for datatypes. Make sygus parsing more l... | ajreynol |
2015-09-18 | More work mixing UF and sygus. | ajreynol |
2015-09-18 | Allow most smt2 commands as sygus commands. Fix bug in fmf-fun regarding quan... | ajreynol |
2015-08-01 | Simplification/improvement to solving deltas in LRA cbqi. Bug fix sygus datat... | ajreynol |
2015-08-01 | Support for default grammar for datatypes in sygus. Support vts for infinity. | ajreynol |
2015-07-31 | Sygus support for inductive datatypes. | ajreynol |
2015-07-25 | Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/... | ajreynol |
2015-07-20 | Squashed merge of SygusComp 2015 branch. | ajreynol |
2015-06-12 | Make sygus an output language. Parse declare-fun in sygus. Minor improvemen... | ajreynol |
2015-06-12 | Accelerate sygus solution reconstruction for constants and id functions. Min... | ajreynol |
2015-06-11 | Avoid naming conflicts in sygus, refactor. Add missing regression. Detect St... | ajreynol |
2015-06-11 | Handle duplicate operators in sygus grammars. Parse sygus quoted literals. A... | ajreynol |
2015-06-11 | Update experimental scripts. Support top-level non-terminals in sygus gramma... | ajreynol |
2015-06-10 | Bug fix parsing constant constructor sygus. | ajreynol |
2015-06-10 | Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w... | ajreynol |
2015-06-10 | Parse support for sygus LetGTerm. | ajreynol |
2015-06-03 | Refactoring of sygus parsing, properly parse Constant/Variable constructors. | ajreynol |
2015-06-02 | Flatten sygus grammars during parsing. Remove duplicate operators from grammars. | ajreynol |
2015-06-02 | Add casc 25 tfn script. Change tff script to output instantiations. Work tow... | ajreynol |
2015-05-28 | added options for controlling resource step-count for various solving stages | Liana Hadarean |
2015-05-11 | Allow sygus with no syntactic restrictions for LIA. Add regressions. | ajreynol |
2015-05-11 | Support for arbitrary constants/variables in Sygus grammars. | ajreynol |
2015-04-24 | More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fm... | ajreynol |
2015-04-24 | Fix sygus parser for non-tokenized operators, reenable regression. Fix for --... | ajreynol |