From 2039eab2d76cf5f4cfe44680f5325f44a4fc5a99 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Tue, 3 Nov 2015 04:47:30 -0500 Subject: cardinality operation for finite sets (based on my thesis / ijcar16 paper) Some further cleanup/fixes pending This is squash of 39 commits (kbansal/card branch + cleanup): * add card operator * local reasoning * towards graph building * first implementation * close cardinality terms * model building * more * more * more * Add aggressive sets rewriting. * Recursively aggressive rewrite sets. * Fix * incomplete card2 implementation * ... * Avoid using auto in sets. * fix merge * more * ... * more * ... * Fixed for loops * Slight modification to computeRelevantTerms * more * .. * more * ... * mv empty set lemma generation to later point * more options/reordering * debug related * more trace * ... * fix merge_nodes, models * rm warnigns * fix compile errors * warning * bug fixes/cleanup * mroe fixes * cleanup * ... --- src/smt/smt_engine_check_proof.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/smt/smt_engine_check_proof.cpp') diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index a58102d86..5634a4651 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -22,7 +22,7 @@ #include #include -#warning "TODO: Why is lfsc's check.h being included like this?" +// #warning "TODO: Why is lfsc's check.h being included like this?" #include "check.h" #include "base/configuration_private.h" -- cgit v1.2.3