cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2014-04-14	Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ↵	Andrew Reynolds
	Improve datatypes rewrite, make option for previous dt semantics.
2014-04-10	Expand definitions in theory datatypes, now has the expected semantics for ↵	Andrew Reynolds
	incorrectly applied selector terms.
2014-04-10	Add support for cardinality constraints logic UFC. Add regressions in fmf/. ↵	Andrew Reynolds
	Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit.
2014-04-09	add tests	Kshitij Bansal

2014-04-09	inputs to trigger bug	Kshitij Bansal

2014-04-06	Reduced example from pcc's bug report.	Tim King

2014-04-06	Merge pull request #21 from pcc/ite-fix	Tim King
	Fix for ite of >=64bit wide bitvectors with unconstrained condition.
2014-04-03	Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis ↵	Morgan Deters
	Deligiannis and Jeroen Ketema for discovering this issue.
2014-04-01	Merge branch '1.3.x'	Tim King

2014-04-01	Fixing bug 552. There was a bug when integers are made using a string with ↵1.3.x	Tim King
	a lot of leading 0s on old versions of CLN.
2014-03-31	add str to u16/u32, and u16/u32 to str	Tianyi Liang

2014-03-28	add construles, type_rules rm redundant, kinds cleanup	Kshitij Bansal

2014-03-27	adds new feature: re.loop	Tianyi Liang

2014-03-20	Merge pull request #22 from kbansal/sets-model	Kshitij Bansal
	Sets model
2014-03-20	cleanup	Kshitij Bansal

2014-03-20	fix for sets/mar2014/..317minimized..	Kshitij Bansal
	Observed behavior: --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143)) with different set of elements in the model for representative and the node itself. Issue: The trouble with data structure being mainted to ensure that things for which lemmas have been generated are not generated again. This data structure (d_pendingEverInserted) needs to be user context dependent. The bug was in the sequence of steps from requesting that a lemma be generated to when it actually was. Sequence was: addToPending (and also adds to pending ever inserted) -> isComplete (might remove things from pending if requirment met in other ways) -> getLemma (actually generated the lemma, if requirement not already met) Resolution: adding terms to d_pendingEverInserted was moved from addToPending() to getLemma().
2014-03-20	Fix for registration issues of term appearing in a shared lemma	Kshitij Bansal
	(brought to attention by lianah -- fix currently just adapted using arrays -- this is to remind me to raise why do we even have this isPreregistered bussiness)
2014-03-20	fix a sharing issues with sets	Kshitij Bansal

2014-03-20	enable check-models for sets/ regressions	Kshitij Bansal

2014-03-20	testlemma regressions	Kshitij Bansal

2014-03-19	Minor usability fixes related to SMT-LIB compliance.	Morgan Deters

2014-03-16	Fix for ite of >=64bit wide bitvectors with unconstrained condition.	Peter Collingbourne

2014-03-12	Work on array pf signature, add working example. Add quantifiers proof ↵	Andrew Reynolds
	signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default.
2014-03-12	Fix LogicInfo unit test.	Morgan Deters

2014-03-12	Some standardization of regression Makefiles that got out of sync. Fixes ↵	Morgan Deters
	cases of nonterminating rewrite-rules regressions.
2014-03-11	Minor cleanup.	Morgan Deters
	* Reenable parts of bvsimple test * Fix typo in #endif comment
2014-03-11	Fix for (get-assignment), resolves bug 553.	Morgan Deters

2014-03-11	Initial refactor of rewrite rules, make theory_rewriterules empty theory. ↵	Andrew Reynolds
	Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter. Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up. QCF is now functional backend to rewrite rules. Support boolean variables in QCF. Change check-model to ignore rewrite rules. Incorporate some fixes from master. Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern. Minor fixes to QCF/rewrite engine, removes RE on last call approach. Add option for one inst per round in RE. Merging rewrite rules into master, check-model current fails on 3 FMF regressions. Fix check-model issue, a line of code was omitted during merge.
2014-03-08	Merge remote-tracking branch 'CVC4root/master'	Tim King

2014-03-07	Remove --ite-remove-quant; support pulling ground ITEs out of quantifier ↵	Morgan Deters
	bodies; fix bug 551, improper ITE removal under quantifiers.
2014-03-07	Fix run_regression on Mac.	Morgan Deters

2014-03-07	Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into ↵	Tim King
	master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.
2014-03-05	Array smtlib compliance tests	Kshitij Bansal

2014-03-05	Revert "fix naming conflicts in benchmarks"	Kshitij Bansal
	This reverts commit 4cac1b63f76a0a973a015ea6f8e21ad31d84d971.
2014-03-05	Don't tokenize SET_THEORY operators in smt2 parser	Kshitij Bansal

2014-03-05	Improving support for POW in arithmetic. Resolves bug 549.	Tim King

2014-03-04	Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas ↵	Morgan Deters
	(resolves bug #548).
2014-02-28	a new regular expression engine for solving both positive and negative ↵	Tianyi Liang
	membership constraints
2014-02-26	sorry for the missing file	Tianyi Liang

2014-02-26	bug fix (caused by merge), move cardinality option to expert option	Tianyi Liang

2014-02-21	Fix makefile dependence for system tests.	Morgan Deters

2014-02-21	disable test cvc3_main, attempt to fix dist_check	Kshitij Bansal

2014-02-21	add new theory (sets)	Kshitij Bansal
	Specification (smt2) -- as per this commit, subject to change - Parameterized sort Set, e.g. (Set Int) - Empty set constant (typed), use with "as" to specify the type, e.g. (as emptyset (Set Int)) - Create a singleton set (setenum X (Set X)) : creates singleton set - Functions/operators (union (Set X) (Set X) (Set X)) (intersection (Set X) (Set X) (Set X)) (setminus (Set X) (Set X) (Set X)) - Predicates (in X (Set X) Bool) : membership (subseteq (Set X) (Set X) Bool) : set containment
2014-02-20	fix makefile	Tianyi Liang

2014-02-20	add more tests, and define int.to.str(NEGATIVE)=""	Tianyi Liang

2014-02-20	add two cases to the regression test	Tianyi Liang

2014-02-19	Merge branch '1.3.x'	Tim King

2014-02-19	Stopping non-linear terms from entering the dio solver. Fixes bug 547.	Tim King

2014-02-10	Fix build (some nonexistent files listed in Makefile)	Morgan Deters

2014-02-09	More complete guess instantiation strategy, cvc4 now typically times out ↵	Andrew Reynolds
	instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc