models for literal_exprt

Daniel Kroening · Daniel Kroening · commit 02c1d1a26fc1 · 2019-04-17T20:44:48.000+01:00
This enables us to use decision_proceduret::get for handles that are
literal_exprt.
diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp
@@ -66,6 +66,10 @@ optionalt<bool> prop_conv_solvert::get_bool(const exprt &expr) const
 
     return prop.l_get(result->second).is_true();
   }
+  else if(expr.id() == ID_literal)
+  {
+    return prop.l_get(to_literal_expr(expr).get_literal()).is_true();
+  }
 
   // sub-expressions
 

Original file line number	Diff line number	Diff line change
`@@ -66,6 +66,10 @@ optionalt<bool> prop_conv_solvert::get_bool(const exprt &expr) const`
`66`	`66`
`67`	`67`	`return prop.l_get(result->second).is_true();`
`68`	`68`	`}`
	`69`	`+ else if(expr.id() == ID_literal)`
	`70`	`+ {`
	`71`	`+ return prop.l_get(to_literal_expr(expr).get_literal()).is_true();`
	`72`	`+ }`
`69`	`73`
`70`	`74`	`// sub-expressions`
`71`	`75`