git.libre-soc.org Git - cvc5.git/search

2020-08-18	Andrew Reynolds	Quantifiers engine stores a pointer to the master equality...	commit \| commitdiff \| tree
2020-08-18	Andrew Reynolds	Split SygusSolver from SmtEngine (#4891)	commit \| commitdiff \| tree
2020-08-18	Andrew Reynolds	Add the relevance manager module (#4894) ...non-linear arithmetic (https://github.com/ajreynol/CVC4/tree/relManager).	commit \| commitdiff \| tree
2020-08-18	Andrew Reynolds	(proof-new) Callbacks for term-context-sensitive terms...	commit \| commitdiff \| tree
2020-08-17	Alex Ozdemir	Add identifier name for side condition. (#4902)	commit \| commitdiff \| tree
2020-08-17	Andres Noetzli	[CI] Update package list (#4906) https://github.com/CVC4/LFSC/commit/1d1c55fa17b08e2bc8...	commit \| commitdiff \| tree
2020-08-17	Andrew Reynolds	Dynamic allocation of equality engine in Theory (#4890)	commit \| commitdiff \| tree
2020-08-17	Andrew Reynolds	(proof-new) Prepare the theory of strings for proof...	commit \| commitdiff \| tree
2020-08-16	Andrew Reynolds	Add non-emptiness to conclusion of positive RE star...	commit \| commitdiff \| tree
2020-08-16	Gereon Kremer	(cad solver) Use the current model as initial assignment...	commit \| commitdiff \| tree
2020-08-15	Andrew Reynolds	Minor cleanup related to notifications (#4898)	commit \| commitdiff \| tree
2020-08-15	Andrew Reynolds	Add finishInit method to PropEngine (#4895)	commit \| commitdiff \| tree
2020-08-15	Andrew Reynolds	(proof-new) Add the strings proof checker (#4858)	commit \| commitdiff \| tree
2020-08-14	Andrew Reynolds	Simplify equality engine notifications (#4896)	commit \| commitdiff \| tree
2020-08-14	E Polgreen	correctly parse sygus lang option (#4884)	commit \| commitdiff \| tree
2020-08-14	Gereon Kremer	Inspect roots to avoid certain resultants (Algorithm...	commit \| commitdiff \| tree
2020-08-13	Andrew Reynolds	Split SmtSolver from SmtEngine (#4880)	commit \| commitdiff \| tree
2020-08-13	Andrew Reynolds	Fixes for corner case of decision tree learning with...	commit \| commitdiff \| tree
2020-08-13	Andrew Reynolds	More basic fix for dumping synth-fun (#4886)	commit \| commitdiff \| tree
2020-08-13	Andrew Reynolds	Add the distributed equality engine manager (#4867)	commit \| commitdiff \| tree
2020-08-13	Haniel Barbosa	[proof-new] Adding support for corner case of transitivity...	commit \| commitdiff \| tree
2020-08-12	Haniel Barbosa	generalize handling MERGED_THROUGH_CONSTANST in EqProof...	commit \| commitdiff \| tree
2020-08-12	Abdalrhman Mohamed	Refactor functions that print commands (Part 1) (#4869)	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	Fixes for degenerate case of sygus decision tree learning...	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	(proof-new) Improve robustness of CONG rule (#4882)	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	(proof-new) Proof support in the strings term registry...	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	(proof-new) Improve interfaces to proof generators...	commit \| commitdiff \| tree
2020-08-12	makaimann	Add option to only build library (#4801)	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	(proof-new) Witness form proof generator (#4782)	commit \| commitdiff \| tree
2020-08-12	Gereon Kremer	Add naive support for integer variables. (#4835)	commit \| commitdiff \| tree
2020-08-12	Haniel Barbosa	(proof-new) Improving proof-production in Equality...	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	Fix connection to master equality engine in sets (...	commit \| commitdiff \| tree
2020-08-12	Gereon Kremer	Fix infinite loop in arith_ite_simp (#4805)	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	Fix unsupported option in regress1. (#4874)	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	Split SmtEngineState from SmtEngine (#4855)	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	Prepare theory of sets for dynamic allocation of equality...	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	Final preparations for changing API to use the Node...	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	(proof-new) Extensions to proof checker interface ...	commit \| commitdiff \| tree
2020-08-11	Andrew Reynolds	Update Expr-level unit tests that depend on datatypes...	commit \| commitdiff \| tree
2020-08-11	Andrew Reynolds	Remove instantiation model true option (#4861)	commit \| commitdiff \| tree
2020-08-11	Aina Niemetz	New C++ API: Remove redundant API functions for mkReal...	commit \| commitdiff \| tree
2020-08-09	Andrew Reynolds	Make valuation class more robust to null underlying...	commit \| commitdiff \| tree
2020-08-09	Andrew Reynolds	Splitting a few utility classes from EqualityEngine...	commit \| commitdiff \| tree
2020-08-08	Andrew Reynolds	Move datatype index constant to its own file (#4859)	commit \| commitdiff \| tree
2020-08-07	Aina Niemetz	GH Actions: Remove cancel action. (#4843)	commit \| commitdiff \| tree
2020-08-06	Andrew Reynolds	Updates not related to creation for eliminating Expr...	commit \| commitdiff \| tree
2020-08-06	Andrew Reynolds	Split preprocessor from SmtEngine (#4854)	commit \| commitdiff \| tree
2020-08-06	Andrew Reynolds	(proof-new) Refactor regular expression operation ...	commit \| commitdiff \| tree
2020-08-05	Andrew Reynolds	Split Assertions from SmtEngine (#4788)	commit \| commitdiff \| tree
2020-08-05	Gereon Kremer	Improve error message for unsupported exponents (#4852)	commit \| commitdiff \| tree
2020-08-05	Andrew V. Jones	When checking models, ensure that error message is...	commit \| commitdiff \| tree
2020-08-05	Andres Noetzli	[Strings] Add eager context-dependent evaluation (...	commit \| commitdiff \| tree
2020-08-05	Gereon Kremer	Add dummy returns if libpoly is unavailable. (#4845)	commit \| commitdiff \| tree
2020-08-04	Andrew Reynolds	Fixes for getInterpolant and getAbduct API methods...	commit \| commitdiff \| tree
2020-08-04	Mathias Preiner	Add documentation and build instructions for recompilation...	commit \| commitdiff \| tree
2020-08-04	Abdalrhman Mohamed	Modify the smt2 parser to use the Sygus grammar. (...	commit \| commitdiff \| tree
2020-08-04	Andrew Reynolds	Add API interface for specialized constructor term...	commit \| commitdiff \| tree
2020-08-04	Gereon Kremer	Properly initialize d_fullyInited. (#4840)	commit \| commitdiff \| tree
2020-08-04	Gereon Kremer	Add CAD-based solver (#4834)	commit \| commitdiff \| tree
2020-08-03	Andres Noetzli	Update documentation for Solver::mkVar() (#4833)	commit \| commitdiff \| tree
2020-08-03	Ying Sheng	Add implementation for SyGuS interpolation module ...	commit \| commitdiff \| tree
2020-08-03	yoni206	New BV rewrite rules aimed at bv_to_int preprocessing...	commit \| commitdiff \| tree
2020-08-03	Andrew Reynolds	Generalize interface for candidate rewrite database...	commit \| commitdiff \| tree
2020-08-03	Andrew Reynolds	Update datatypes in cvc parser to the new API (#4826)	commit \| commitdiff \| tree
2020-08-03	yoni206	Examples for using sygus python api (#4822)	commit \| commitdiff \| tree
2020-08-03	makaimann	Delete solver pointer in Cython __dealloc__ (#4799)	commit \| commitdiff \| tree
2020-08-03	Andrew Reynolds	Split expression names from SmtEngine (#4832)	commit \| commitdiff \| tree
2020-08-03	Andrew Reynolds	Split dump manager from SmtEngine (#4824)	commit \| commitdiff \| tree
2020-08-02	Andrew Reynolds	Updates to dtype constructor in preparation for eliminating...	commit \| commitdiff \| tree
2020-08-02	Andres Noetzli	Fix ASan failure in interactive_shell_black (#4827)	commit \| commitdiff \| tree
2020-08-02	Andres Noetzli	Ensure strict length constraint for decompose rule...	commit \| commitdiff \| tree
2020-08-02	Andrew Reynolds	Add methods for constructing datatype types from NodeManager...	commit \| commitdiff \| tree
2020-08-01	Andrew V. Jones	Ensure that we only find '.a's when building statically...	commit \| commitdiff \| tree
2020-08-01	Andrew Reynolds	Fix component contains for splicing due to substring...	commit \| commitdiff \| tree
2020-08-01	yoni206	Add SyGuS Python API (#4812)	commit \| commitdiff \| tree
2020-07-31	Andrew Reynolds	Split listener classes from SmtEngine (#4816)	commit \| commitdiff \| tree
2020-07-31	Andrew Reynolds	Standardize explanations in arrays (#4804)	commit \| commitdiff \| tree
2020-07-30	Andres Noetzli	Python API: Add support for sequences (#4757)	commit \| commitdiff \| tree
2020-07-30	Gereon Kremer	Cad implementation (#4774)	commit \| commitdiff \| tree
2020-07-30	Gereon Kremer	Adds the interface for the CAD-based arithmetic solver...	commit \| commitdiff \| tree
2020-07-30	Andrew V. Jones	When linking Editline, use 'pkg-config' to correctly...	commit \| commitdiff \| tree
2020-07-30	Andrew Reynolds	Fix null case for sygus printing (#4793)	commit \| commitdiff \| tree
2020-07-30	Andrew Reynolds	(proof-new) Stream output for ProofNode (#4789)	commit \| commitdiff \| tree
2020-07-30	Andrew Reynolds	(proof-new) Fixes for getFreeAssumptions (#4802)	commit \| commitdiff \| tree
2020-07-28	Ying Sheng	fixing issue #4808. (#4810)	commit \| commitdiff \| tree
2020-07-28	Andrew Reynolds	Remove arrays lazy rintro option (#4806)	commit \| commitdiff \| tree
2020-07-28	Andres Noetzli	Replace Expr with Node in Term/Op (#4781)	commit \| commitdiff \| tree
2020-07-28	Andrew Reynolds	Fix regular expression delta for complement (#4765)	commit \| commitdiff \| tree
2020-07-28	yoni206	Supporting seq.nth (#4723)	commit \| commitdiff \| tree
2020-07-28	Ying Sheng	Interpolation: Add interface for SyGuS interpolation...	commit \| commitdiff \| tree
2020-07-28	Andrew Reynolds	Use lemma property enum for OutputChannel::lemma (...	commit \| commitdiff \| tree
2020-07-27	Andrew Reynolds	(proof-new) Proof production for term formula removal...	commit \| commitdiff \| tree
2020-07-27	Andrew Reynolds	(proof-new) Arithmetic operator elim proof producing...	commit \| commitdiff \| tree
2020-07-27	Alex Ozdemir	Consider negation's proof before triggering arith pfs...	commit \| commitdiff \| tree
2020-07-21	Aina Niemetz	GH Actions: Cancel builds on push, remove redundant...	commit \| commitdiff \| tree
2020-07-21	Andrew Reynolds	Support uninterpreted constants in the evaluator (...	commit \| commitdiff \| tree
2020-07-21	Gereon Kremer	Preparations for a CAD-based arithmetic solver (#4762)	commit \| commitdiff \| tree
2020-07-20	Alex Ozdemir	Fix a deadlock in the signature tests. (#4772) ...a duplicate of [this](https://github.com/CVC4/LFSC/pull/38).	commit \| commitdiff \| tree
2020-07-18	Haniel Barbosa	Improving equality engine tracing (#4770)	commit \| commitdiff \| tree
2020-07-18	Andrew Reynolds	(proof-new) Proof recording for assertions pipeline...	commit \| commitdiff \| tree
next

RSS Atom