From 2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 8 Nov 2016 10:09:53 -0600 Subject: Add a few options to separation logic and sets. Minor changes to separation logic, change syntax for empty heap constraint. --- src/options/sep_options | 6 ++++++ src/options/sets_options | 18 ++---------------- 2 files changed, 8 insertions(+), 16 deletions(-) (limited to 'src/options') diff --git a/src/options/sep_options b/src/options/sep_options index fecf4401e..ba10cdefb 100644 --- a/src/options/sep_options +++ b/src/options/sep_options @@ -15,4 +15,10 @@ option sepMinimalRefine --sep-min-refine bool :default false option sepDisequalC --sep-deq-c bool :default true assume cardinality elements are distinct +option sepPreSkolemEmp --sep-pre-skolem-emp bool :default false + eliminate emp constraint at preprocess time + +option sepChildRefine --sep-child-refine bool :default false + child-specific refinements of negated star, positive wand + endmodule diff --git a/src/options/sets_options b/src/options/sets_options index 4c019c039..52a8f78ba 100644 --- a/src/options/sets_options +++ b/src/options/sets_options @@ -5,22 +5,8 @@ module SETS "options/sets_options.h" Sets -option setsPropagate --sets-propagate bool :default true - determines whether to propagate learnt facts to Theory Engine / SAT solver - -option setsEagerLemmas --sets-eager-lemmas bool :default true - add lemmas even at regular effort - -expert-option setsCare1 --sets-care1 bool :default false - generate one lemma at a time for care graph - -option setsPropFull --sets-prop-full bool :default true - additional propagation at full effort - -option setsGuessEmpty --sets-guess-empty int :default 0 - when to guess leaf nodes being empty (0...2 : most aggressive..least aggressive) - -option setsSlowLemmas --sets-slow-lemmas bool :default true +option setsProxyLemmas --sets-proxy-lemmas bool :default false + introduce proxy variables eagerly to shorten lemmas option setsInferAsLemmas --sets-infer-as-lemmas bool :default true send inferences as lemmas -- cgit v1.2.3