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

2020-03-06	Andres Noetzli	Ignore model check warning in regression test (#3926)	commit \| commitdiff \| tree
2020-03-06	Andrew Reynolds	Make sygus datatype building independent of parser...	commit \| commitdiff \| tree
2020-03-06	Andrew Reynolds	Support default sygus grammar construction for sets...	commit \| commitdiff \| tree
2020-03-06	Andres Noetzli	Make output of regression script more readable (#3911)	commit \| commitdiff \| tree
2020-03-06	Andres Noetzli	Remove --apply-to-const preprocessing pass (#3919)	commit \| commitdiff \| tree
2020-03-05	Andres Noetzli	Add a new arith constraint proof rule: IntTightenAP...	commit \| commitdiff \| tree
2020-03-05	Andrew Reynolds	Migrate a majority of the functionality in parsers...	commit \| commitdiff \| tree
2020-03-05	Andrew Reynolds	Move ownership of DecisionEngine into PropEngine. ...	commit \| commitdiff \| tree
2020-03-05	Andrew Reynolds	Fix issues with real to int (#3918)	commit \| commitdiff \| tree
2020-03-05	Mathias Preiner	Enable -Wshadow and fix warnings. (#3909) ...yoni206 <yoni206@users.noreply.github.com> ...Donovick <cdonovick@users.noreply.github.com>	commit \| commitdiff \| tree
2020-03-03	mudathirmahgoub	Refactoring and cleaning the type enumerator for sets...	commit \| commitdiff \| tree
2020-03-03	Andrew Reynolds	Standardize the interface for SMT engine subsolvers...	commit \| commitdiff \| tree
2020-03-03	Andres Noetzli	Fix `TheorySetsPrive::eqNotifyPostMerge()` (#3901)	commit \| commitdiff \| tree
2020-03-03	Mathias Preiner	Fix variable shadowing bug in sets. (#3898)	commit \| commitdiff \| tree
2020-03-02	Andrew Reynolds	Split collect model info by types in strings (#3847)	commit \| commitdiff \| tree
2020-02-29	Andrew Reynolds	Convert more uses of string to word (#3834)	commit \| commitdiff \| tree
2020-02-29	Andrew Reynolds	Throw warning instead of error for non-constant values...	commit \| commitdiff \| tree
2020-02-29	Andres Noetzli	Add support for str.from_code (#3829)	commit \| commitdiff \| tree
2020-02-29	Aina Niemetz	propEngine: Reorder class declaration according to...	commit \| commitdiff \| tree
2020-02-29	Andrew Reynolds	Fix assertion related to assignability in the model...	commit \| commitdiff \| tree
2020-02-29	Andrew Reynolds	Replace conditional rewrite pass in quantifiers with...	commit \| commitdiff \| tree
2020-02-28	Andrew Reynolds	Use enum for quantifiers rewrite steps (#3840)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Refactor operator applications in the parser (#3831)	commit \| commitdiff \| tree
2020-02-27	Haniel Barbosa	Changing TPTP parser to accomodate new API (#3837)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Update purifySygusGTerm to the new API (#3830)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Fix large models for strings (#3835)	commit \| commitdiff \| tree
2020-02-27	Andres Noetzli	Fix -Wshadow warnings in common headers (#3826)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Add support for is_digit and regular expression difference...	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Disable regression that times out on debug (#3833)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Move fix for vacuous sygus types out of the parser...	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Initial work towards -Wshadow (#3817)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Some initial work on using words (#3819)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Infrastructure for tautological literals in nonlinear...	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Use side effect utility for non-linear lemmas (#3780)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Fix regression (#3827)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	More fixes for printing sygus commands (#3812)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Basic support for regular expression complement (#3437)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Refactor type ascriptions in the parser (#3825)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Minor improvement to ParseOp (#3808)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Use default consts when not using any const during...	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Fix node arity issue in reduction of int2bv (#3777)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Move equivalence class info to its own file in strings...	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Support for witnessing choice in models (#3781)	commit \| commitdiff \| tree
2020-02-26	Andres Noetzli	Remove portfolio leftovers (#3821)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Minor cleaning of smt2 parser (#3823)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Embed mkAssociative utilities within the API. (#3801)	commit \| commitdiff \| tree
2020-02-25	mudathirmahgoub	Sets & Relations Java example (#3816) Fixes [(Bugzilla #677)](https://github.com/CVC4/cvc4-projects/issues...	commit \| commitdiff \| tree
2020-02-25	mudathirmahgoub	Sets & Relations Java example (#3816)	commit \| commitdiff \| tree
2020-02-25	yoni206	remove redundant includes (#3815)	commit \| commitdiff \| tree
2020-02-25	yoni206	bv_to_int preprocessing pass	commit \| commitdiff \| tree
2020-02-24	Andrew Reynolds	Fixes for quantifiers documentation (#3811)	commit \| commitdiff \| tree
2020-02-24	Andrew Reynolds	Utilities for words (#3797)	commit \| commitdiff \| tree
2020-02-24	Andrew Reynolds	Convert parser input interface to api::Term (#3809)	commit \| commitdiff \| tree
2020-02-24	Abdalrhman Mohamed	Fix bugs related to printing Sygus commands (#3804)	commit \| commitdiff \| tree
2020-02-24	Andrew Reynolds	Add missing functions to new C++ API (#3769)	commit \| commitdiff \| tree
2020-02-24	Andres Noetzli	Make lambda rewriter more robust (#3806)	commit \| commitdiff \| tree
2020-02-23	Andrew Reynolds	Minor refactoring of equality notifications (#3798)	commit \| commitdiff \| tree
2020-02-22	Alex Ozdemir	RIP th_lra.plf (#3796)	commit \| commitdiff \| tree
2020-02-22	Andrew Reynolds	Move check memberships to reg exp solver (#3793)	commit \| commitdiff \| tree
2020-02-22	Andrew Reynolds	Move cardinality inference scheme to base solver in...	commit \| commitdiff \| tree
2020-02-22	makaimann	Dump boolean propagations and conflicts for decision...	commit \| commitdiff \| tree
2020-02-22	Alex Ozdemir	Switch to th_lira.plf (#3741)	commit \| commitdiff \| tree
2020-02-21	Aina Niemetz	New C++ API: Remove TOTAL kinds. (#3794)	commit \| commitdiff \| tree
2020-02-21	Andrew Reynolds	Simple changes towards unicode string standard (#3791)	commit \| commitdiff \| tree
2020-02-21	Andrew V. Jones	Adding checks to the validation of 'bv-sat-solver'...	commit \| commitdiff \| tree
2020-02-21	Andrew Reynolds	Split extended functions solver in strings (#3768)	commit \| commitdiff \| tree
2020-02-21	Alex Ozdemir	Remove IntReal tightening axioms from th_lira.plf ...	commit \| commitdiff \| tree
2020-02-20	Andrew Reynolds	Remove front-end support for Chain (#3767)	commit \| commitdiff \| tree
2020-02-20	Andres Noetzli	Remove unused code (#3782)	commit \| commitdiff \| tree
2020-02-20	Andrew Reynolds	Minor removals (#3786)	commit \| commitdiff \| tree
2020-02-20	Andres Noetzli	Remove parser from bindings (#3779)	commit \| commitdiff \| tree
2020-02-20	Mathias Preiner	resource manager: Add statistic for every resource...	commit \| commitdiff \| tree
2020-02-19	Andrew Reynolds	Fix symmetry breaking for multiple sygus types (#3775)	commit \| commitdiff \| tree
2020-02-19	makaimann	Add Python bindings using Cython -- see below for more...	commit \| commitdiff \| tree
2020-02-19	Andrew Reynolds	Delay enumerative instantiation if theory engine does...	commit \| commitdiff \| tree
2020-02-19	Andrew Reynolds	Change Record to shared_ptr (#3778)	commit \| commitdiff \| tree
2020-02-19	Andrew Reynolds	Fix approximate bounds for transcendental functions... ...43099566+ahmed-irfan@users.noreply.github.com>	commit \| commitdiff \| tree
2020-02-19	makaimann	Change datatype selector/constructor/tester to terms...	commit \| commitdiff \| tree
2020-02-18	Andrew Reynolds	Add missing kinds for the new API (#3757)	commit \| commitdiff \| tree
2020-02-17	Andrew Reynolds	Option to limit the number of rounds of enumerative...	commit \| commitdiff \| tree
2020-02-17	Andrew Reynolds	Fix soundness bug in reduction of integer div/mod... ...introduced 7 years ago in https://github.com/CVC4/CVC4/commit/9098391fe334d829ec...	commit \| commitdiff \| tree
2020-02-17	Haniel Barbosa	Using ParseOp in TPTP (#3764)	commit \| commitdiff \| tree
2020-02-17	Abdalrhman Mohamed	Support dumping Sygus commands. (#3763)	commit \| commitdiff \| tree
2020-02-16	Andrew Reynolds	Fix simple issue with cache (#3762)	commit \| commitdiff \| tree
2020-02-16	Andrew Reynolds	Add temporary global API conversion utilities. (#3759)	commit \| commitdiff \| tree
2020-02-16	Andres Noetzli	Activate reverse variant of F-Split inference (#3745)	commit \| commitdiff \| tree
2020-02-16	Andrew Reynolds	Disable regression (#3761)	commit \| commitdiff \| tree
2020-02-15	Andrew Reynolds	Move proxy variables to InferenceManager in strings...	commit \| commitdiff \| tree
2020-02-14	Andrew Reynolds	Remove quantifiers rewrite rules infrastructure (#3754)	commit \| commitdiff \| tree
2020-02-14	Andrew Reynolds	Update sygus v1 parser to use ParseOp utility (#3756)	commit \| commitdiff \| tree
2020-02-14	Haniel Barbosa	Forcing rewrite pass rather than asserting if formula...	commit \| commitdiff \| tree
2020-02-13	Andrew Reynolds	Const input for sygus print callback (#3755)	commit \| commitdiff \| tree
2020-02-13	Andres Noetzli	[Python] Properly destroy CVC4 object (#3753)	commit \| commitdiff \| tree
2020-02-12	Andres Noetzli	Rename Java package to edu.stanford.CVC4 (#3752)	commit \| commitdiff \| tree
2020-02-12	Andrew Reynolds	Ensure ext rewrites for associative ops dont throw...	commit \| commitdiff \| tree
2020-02-12	Mathias Preiner	run_regression: Distinguish between timeout and failure...	commit \| commitdiff \| tree
2020-02-12	Andrew Reynolds	Fix non-linear equality solving that involves mixed... ...43099566+ahmed-irfan@users.noreply.github.com>	commit \| commitdiff \| tree
2020-02-11	Mathias Preiner	cmake: Remove unused ENABLE_OPTIMIZED option. (#3749)	commit \| commitdiff \| tree
2020-02-11	Andrew Reynolds	Fix term simplification based on entailment in quantifiers...	commit \| commitdiff \| tree
2020-02-11	Mathias Preiner	Update issue templates	commit \| commitdiff \| tree
next

RSS Atom